(0) Obligation:

Clauses:

log2(X, Y) :- log2(X, 0, Y).
log2(0, I, I).
log2(s(0), I, I).
log2(s(s(X)), I, Y) :- ','(half(s(s(X)), X1), log2(X1, s(I), Y)).
half(0, 0).
half(s(0), 0).
half(s(s(X)), s(Y)) :- half(X, Y).

Query: log2(g,a)

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

(2) Obligation:

Clauses:

halfA(0, 0).
halfA(s(0), 0).
halfA(s(s(T21)), s(X44)) :- halfA(T21, X44).
halfB(T18, s(X35)) :- halfA(T18, X35).
pC(T74, X205, T77, T76) :- halfB(T74, X205).
pC(T74, 0, T85, s(T85)) :- halfB(T74, 0).
pC(T74, s(0), T90, s(T90)) :- halfB(T74, s(0)).
pC(T74, s(s(T97)), T98, T100) :- ','(halfB(T74, s(s(T97))), pC(T97, X228, s(T98), T100)).
log2D(0, 0).
log2D(s(0), 0).
log2D(s(s(T12)), T14) :- halfB(T12, X26).
log2D(s(s(T12)), s(0)) :- halfB(T12, 0).
log2D(s(s(T12)), s(0)) :- halfB(T12, s(0)).
log2D(s(s(T12)), T28) :- ','(halfB(T12, s(s(T26))), halfB(T26, X67)).
log2D(s(s(T12)), s(s(0))) :- ','(halfB(T12, s(s(T26))), halfB(T26, 0)).
log2D(s(s(T12)), s(s(0))) :- ','(halfB(T12, s(s(T26))), halfB(T26, s(0))).
log2D(s(s(T12)), T36) :- ','(halfB(T12, s(s(T26))), ','(halfB(T26, s(s(T34))), halfB(T34, X90))).
log2D(s(s(T12)), s(s(s(0)))) :- ','(halfB(T12, s(s(T26))), ','(halfB(T26, s(s(T34))), halfB(T34, 0))).
log2D(s(s(T12)), s(s(s(0)))) :- ','(halfB(T12, s(s(T26))), ','(halfB(T26, s(s(T34))), halfB(T34, s(0)))).
log2D(s(s(T12)), T44) :- ','(halfB(T12, s(s(T26))), ','(halfB(T26, s(s(T34))), ','(halfB(T34, s(s(T42))), halfB(T42, X113)))).
log2D(s(s(T12)), s(s(s(s(0))))) :- ','(halfB(T12, s(s(T26))), ','(halfB(T26, s(s(T34))), ','(halfB(T34, s(s(T42))), halfB(T42, 0)))).
log2D(s(s(T12)), s(s(s(s(0))))) :- ','(halfB(T12, s(s(T26))), ','(halfB(T26, s(s(T34))), ','(halfB(T34, s(s(T42))), halfB(T42, s(0))))).
log2D(s(s(T12)), T52) :- ','(halfB(T12, s(s(T26))), ','(halfB(T26, s(s(T34))), ','(halfB(T34, s(s(T42))), ','(halfB(T42, s(s(T50))), halfB(T50, X136))))).
log2D(s(s(T12)), s(s(s(s(s(0)))))) :- ','(halfB(T12, s(s(T26))), ','(halfB(T26, s(s(T34))), ','(halfB(T34, s(s(T42))), ','(halfB(T42, s(s(T50))), halfB(T50, 0))))).
log2D(s(s(T12)), s(s(s(s(s(0)))))) :- ','(halfB(T12, s(s(T26))), ','(halfB(T26, s(s(T34))), ','(halfB(T34, s(s(T42))), ','(halfB(T42, s(s(T50))), halfB(T50, s(0)))))).
log2D(s(s(T12)), T60) :- ','(halfB(T12, s(s(T26))), ','(halfB(T26, s(s(T34))), ','(halfB(T34, s(s(T42))), ','(halfB(T42, s(s(T50))), ','(halfB(T50, s(s(T58))), halfB(T58, X159)))))).
log2D(s(s(T12)), s(s(s(s(s(s(0))))))) :- ','(halfB(T12, s(s(T26))), ','(halfB(T26, s(s(T34))), ','(halfB(T34, s(s(T42))), ','(halfB(T42, s(s(T50))), ','(halfB(T50, s(s(T58))), halfB(T58, 0)))))).
log2D(s(s(T12)), s(s(s(s(s(s(0))))))) :- ','(halfB(T12, s(s(T26))), ','(halfB(T26, s(s(T34))), ','(halfB(T34, s(s(T42))), ','(halfB(T42, s(s(T50))), ','(halfB(T50, s(s(T58))), halfB(T58, s(0))))))).
log2D(s(s(T12)), T68) :- ','(halfB(T12, s(s(T26))), ','(halfB(T26, s(s(T34))), ','(halfB(T34, s(s(T42))), ','(halfB(T42, s(s(T50))), ','(halfB(T50, s(s(T58))), ','(halfB(T58, s(s(T66))), halfB(T66, X182))))))).
log2D(s(s(T12)), s(s(s(s(s(s(s(0)))))))) :- ','(halfB(T12, s(s(T26))), ','(halfB(T26, s(s(T34))), ','(halfB(T34, s(s(T42))), ','(halfB(T42, s(s(T50))), ','(halfB(T50, s(s(T58))), ','(halfB(T58, s(s(T66))), halfB(T66, 0))))))).
log2D(s(s(T12)), s(s(s(s(s(s(s(0)))))))) :- ','(halfB(T12, s(s(T26))), ','(halfB(T26, s(s(T34))), ','(halfB(T34, s(s(T42))), ','(halfB(T42, s(s(T50))), ','(halfB(T50, s(s(T58))), ','(halfB(T58, s(s(T66))), halfB(T66, s(0)))))))).
log2D(s(s(T12)), T76) :- ','(halfB(T12, s(s(T26))), ','(halfB(T26, s(s(T34))), ','(halfB(T34, s(s(T42))), ','(halfB(T42, s(s(T50))), ','(halfB(T50, s(s(T58))), ','(halfB(T58, s(s(T66))), ','(halfB(T66, s(s(T74))), pC(T74, X205, s(s(s(s(s(s(s(0))))))), T76)))))))).

Query: log2D(g,a)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
log2D_in: (b,f)
halfB_in: (b,f) (b,b)
halfA_in: (b,f) (b,b)
pC_in: (b,f,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

log2D_in_ga(0, 0) → log2D_out_ga(0, 0)
log2D_in_ga(s(0), 0) → log2D_out_ga(s(0), 0)
log2D_in_ga(s(s(T12)), T14) → U8_ga(T12, T14, halfB_in_ga(T12, X26))
halfB_in_ga(T18, s(X35)) → U2_ga(T18, X35, halfA_in_ga(T18, X35))
halfA_in_ga(0, 0) → halfA_out_ga(0, 0)
halfA_in_ga(s(0), 0) → halfA_out_ga(s(0), 0)
halfA_in_ga(s(s(T21)), s(X44)) → U1_ga(T21, X44, halfA_in_ga(T21, X44))
U1_ga(T21, X44, halfA_out_ga(T21, X44)) → halfA_out_ga(s(s(T21)), s(X44))
U2_ga(T18, X35, halfA_out_ga(T18, X35)) → halfB_out_ga(T18, s(X35))
U8_ga(T12, T14, halfB_out_ga(T12, X26)) → log2D_out_ga(s(s(T12)), T14)
log2D_in_ga(s(s(T12)), s(0)) → U9_ga(T12, halfB_in_gg(T12, 0))
halfB_in_gg(T18, s(X35)) → U2_gg(T18, X35, halfA_in_gg(T18, X35))
halfA_in_gg(0, 0) → halfA_out_gg(0, 0)
halfA_in_gg(s(0), 0) → halfA_out_gg(s(0), 0)
halfA_in_gg(s(s(T21)), s(X44)) → U1_gg(T21, X44, halfA_in_gg(T21, X44))
U1_gg(T21, X44, halfA_out_gg(T21, X44)) → halfA_out_gg(s(s(T21)), s(X44))
U2_gg(T18, X35, halfA_out_gg(T18, X35)) → halfB_out_gg(T18, s(X35))
U9_ga(T12, halfB_out_gg(T12, 0)) → log2D_out_ga(s(s(T12)), s(0))
log2D_in_ga(s(s(T12)), s(0)) → U10_ga(T12, halfB_in_gg(T12, s(0)))
U10_ga(T12, halfB_out_gg(T12, s(0))) → log2D_out_ga(s(s(T12)), s(0))
log2D_in_ga(s(s(T12)), T28) → U11_ga(T12, T28, halfB_in_ga(T12, s(s(T26))))
U11_ga(T12, T28, halfB_out_ga(T12, s(s(T26)))) → U12_ga(T12, T28, halfB_in_ga(T26, X67))
U12_ga(T12, T28, halfB_out_ga(T26, X67)) → log2D_out_ga(s(s(T12)), T28)
log2D_in_ga(s(s(T12)), s(s(0))) → U13_ga(T12, halfB_in_ga(T12, s(s(T26))))
U13_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U14_ga(T12, halfB_in_gg(T26, 0))
U14_ga(T12, halfB_out_gg(T26, 0)) → log2D_out_ga(s(s(T12)), s(s(0)))
U13_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U15_ga(T12, halfB_in_gg(T26, s(0)))
U15_ga(T12, halfB_out_gg(T26, s(0))) → log2D_out_ga(s(s(T12)), s(s(0)))
log2D_in_ga(s(s(T12)), T36) → U16_ga(T12, T36, halfB_in_ga(T12, s(s(T26))))
U16_ga(T12, T36, halfB_out_ga(T12, s(s(T26)))) → U17_ga(T12, T36, halfB_in_ga(T26, s(s(T34))))
U17_ga(T12, T36, halfB_out_ga(T26, s(s(T34)))) → U18_ga(T12, T36, halfB_in_ga(T34, X90))
U18_ga(T12, T36, halfB_out_ga(T34, X90)) → log2D_out_ga(s(s(T12)), T36)
log2D_in_ga(s(s(T12)), s(s(s(0)))) → U19_ga(T12, halfB_in_ga(T12, s(s(T26))))
U19_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U20_ga(T12, halfB_in_ga(T26, s(s(T34))))
U20_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U21_ga(T12, halfB_in_gg(T34, 0))
U21_ga(T12, halfB_out_gg(T34, 0)) → log2D_out_ga(s(s(T12)), s(s(s(0))))
U20_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U22_ga(T12, halfB_in_gg(T34, s(0)))
U22_ga(T12, halfB_out_gg(T34, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(0))))
log2D_in_ga(s(s(T12)), T44) → U23_ga(T12, T44, halfB_in_ga(T12, s(s(T26))))
U23_ga(T12, T44, halfB_out_ga(T12, s(s(T26)))) → U24_ga(T12, T44, halfB_in_ga(T26, s(s(T34))))
U24_ga(T12, T44, halfB_out_ga(T26, s(s(T34)))) → U25_ga(T12, T44, halfB_in_ga(T34, s(s(T42))))
U25_ga(T12, T44, halfB_out_ga(T34, s(s(T42)))) → U26_ga(T12, T44, halfB_in_ga(T42, X113))
U26_ga(T12, T44, halfB_out_ga(T42, X113)) → log2D_out_ga(s(s(T12)), T44)
log2D_in_ga(s(s(T12)), s(s(s(s(0))))) → U27_ga(T12, halfB_in_ga(T12, s(s(T26))))
U27_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U28_ga(T12, halfB_in_ga(T26, s(s(T34))))
U28_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U29_ga(T12, halfB_in_ga(T34, s(s(T42))))
U29_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U30_ga(T12, halfB_in_gg(T42, 0))
U30_ga(T12, halfB_out_gg(T42, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(0)))))
U29_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U31_ga(T12, halfB_in_gg(T42, s(0)))
U31_ga(T12, halfB_out_gg(T42, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(0)))))
log2D_in_ga(s(s(T12)), T52) → U32_ga(T12, T52, halfB_in_ga(T12, s(s(T26))))
U32_ga(T12, T52, halfB_out_ga(T12, s(s(T26)))) → U33_ga(T12, T52, halfB_in_ga(T26, s(s(T34))))
U33_ga(T12, T52, halfB_out_ga(T26, s(s(T34)))) → U34_ga(T12, T52, halfB_in_ga(T34, s(s(T42))))
U34_ga(T12, T52, halfB_out_ga(T34, s(s(T42)))) → U35_ga(T12, T52, halfB_in_ga(T42, s(s(T50))))
U35_ga(T12, T52, halfB_out_ga(T42, s(s(T50)))) → U36_ga(T12, T52, halfB_in_ga(T50, X136))
U36_ga(T12, T52, halfB_out_ga(T50, X136)) → log2D_out_ga(s(s(T12)), T52)
log2D_in_ga(s(s(T12)), s(s(s(s(s(0)))))) → U37_ga(T12, halfB_in_ga(T12, s(s(T26))))
U37_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U38_ga(T12, halfB_in_ga(T26, s(s(T34))))
U38_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U39_ga(T12, halfB_in_ga(T34, s(s(T42))))
U39_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U40_ga(T12, halfB_in_ga(T42, s(s(T50))))
U40_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U41_ga(T12, halfB_in_gg(T50, 0))
U41_ga(T12, halfB_out_gg(T50, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(0))))))
U40_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U42_ga(T12, halfB_in_gg(T50, s(0)))
U42_ga(T12, halfB_out_gg(T50, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(0))))))
log2D_in_ga(s(s(T12)), T60) → U43_ga(T12, T60, halfB_in_ga(T12, s(s(T26))))
U43_ga(T12, T60, halfB_out_ga(T12, s(s(T26)))) → U44_ga(T12, T60, halfB_in_ga(T26, s(s(T34))))
U44_ga(T12, T60, halfB_out_ga(T26, s(s(T34)))) → U45_ga(T12, T60, halfB_in_ga(T34, s(s(T42))))
U45_ga(T12, T60, halfB_out_ga(T34, s(s(T42)))) → U46_ga(T12, T60, halfB_in_ga(T42, s(s(T50))))
U46_ga(T12, T60, halfB_out_ga(T42, s(s(T50)))) → U47_ga(T12, T60, halfB_in_ga(T50, s(s(T58))))
U47_ga(T12, T60, halfB_out_ga(T50, s(s(T58)))) → U48_ga(T12, T60, halfB_in_ga(T58, X159))
U48_ga(T12, T60, halfB_out_ga(T58, X159)) → log2D_out_ga(s(s(T12)), T60)
log2D_in_ga(s(s(T12)), s(s(s(s(s(s(0))))))) → U49_ga(T12, halfB_in_ga(T12, s(s(T26))))
U49_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U50_ga(T12, halfB_in_ga(T26, s(s(T34))))
U50_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U51_ga(T12, halfB_in_ga(T34, s(s(T42))))
U51_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U52_ga(T12, halfB_in_ga(T42, s(s(T50))))
U52_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U53_ga(T12, halfB_in_ga(T50, s(s(T58))))
U53_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U54_ga(T12, halfB_in_gg(T58, 0))
U54_ga(T12, halfB_out_gg(T58, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
U53_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U55_ga(T12, halfB_in_gg(T58, s(0)))
U55_ga(T12, halfB_out_gg(T58, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
log2D_in_ga(s(s(T12)), T68) → U56_ga(T12, T68, halfB_in_ga(T12, s(s(T26))))
U56_ga(T12, T68, halfB_out_ga(T12, s(s(T26)))) → U57_ga(T12, T68, halfB_in_ga(T26, s(s(T34))))
U57_ga(T12, T68, halfB_out_ga(T26, s(s(T34)))) → U58_ga(T12, T68, halfB_in_ga(T34, s(s(T42))))
U58_ga(T12, T68, halfB_out_ga(T34, s(s(T42)))) → U59_ga(T12, T68, halfB_in_ga(T42, s(s(T50))))
U59_ga(T12, T68, halfB_out_ga(T42, s(s(T50)))) → U60_ga(T12, T68, halfB_in_ga(T50, s(s(T58))))
U60_ga(T12, T68, halfB_out_ga(T50, s(s(T58)))) → U61_ga(T12, T68, halfB_in_ga(T58, s(s(T66))))
U61_ga(T12, T68, halfB_out_ga(T58, s(s(T66)))) → U62_ga(T12, T68, halfB_in_ga(T66, X182))
U62_ga(T12, T68, halfB_out_ga(T66, X182)) → log2D_out_ga(s(s(T12)), T68)
log2D_in_ga(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → U63_ga(T12, halfB_in_ga(T12, s(s(T26))))
U63_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U64_ga(T12, halfB_in_ga(T26, s(s(T34))))
U64_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U65_ga(T12, halfB_in_ga(T34, s(s(T42))))
U65_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U66_ga(T12, halfB_in_ga(T42, s(s(T50))))
U66_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U67_ga(T12, halfB_in_ga(T50, s(s(T58))))
U67_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U68_ga(T12, halfB_in_ga(T58, s(s(T66))))
U68_ga(T12, halfB_out_ga(T58, s(s(T66)))) → U69_ga(T12, halfB_in_gg(T66, 0))
U69_ga(T12, halfB_out_gg(T66, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
U68_ga(T12, halfB_out_ga(T58, s(s(T66)))) → U70_ga(T12, halfB_in_gg(T66, s(0)))
U70_ga(T12, halfB_out_gg(T66, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
log2D_in_ga(s(s(T12)), T76) → U71_ga(T12, T76, halfB_in_ga(T12, s(s(T26))))
U71_ga(T12, T76, halfB_out_ga(T12, s(s(T26)))) → U72_ga(T12, T76, halfB_in_ga(T26, s(s(T34))))
U72_ga(T12, T76, halfB_out_ga(T26, s(s(T34)))) → U73_ga(T12, T76, halfB_in_ga(T34, s(s(T42))))
U73_ga(T12, T76, halfB_out_ga(T34, s(s(T42)))) → U74_ga(T12, T76, halfB_in_ga(T42, s(s(T50))))
U74_ga(T12, T76, halfB_out_ga(T42, s(s(T50)))) → U75_ga(T12, T76, halfB_in_ga(T50, s(s(T58))))
U75_ga(T12, T76, halfB_out_ga(T50, s(s(T58)))) → U76_ga(T12, T76, halfB_in_ga(T58, s(s(T66))))
U76_ga(T12, T76, halfB_out_ga(T58, s(s(T66)))) → U77_ga(T12, T76, halfB_in_ga(T66, s(s(T74))))
U77_ga(T12, T76, halfB_out_ga(T66, s(s(T74)))) → U78_ga(T12, T76, pC_in_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76))
pC_in_gaga(T74, X205, T77, T76) → U3_gaga(T74, X205, T77, T76, halfB_in_ga(T74, X205))
U3_gaga(T74, X205, T77, T76, halfB_out_ga(T74, X205)) → pC_out_gaga(T74, X205, T77, T76)
pC_in_gaga(T74, 0, T85, s(T85)) → U4_gaga(T74, T85, halfB_in_gg(T74, 0))
U4_gaga(T74, T85, halfB_out_gg(T74, 0)) → pC_out_gaga(T74, 0, T85, s(T85))
pC_in_gaga(T74, s(0), T90, s(T90)) → U5_gaga(T74, T90, halfB_in_gg(T74, s(0)))
U5_gaga(T74, T90, halfB_out_gg(T74, s(0))) → pC_out_gaga(T74, s(0), T90, s(T90))
pC_in_gaga(T74, s(s(T97)), T98, T100) → U6_gaga(T74, T97, T98, T100, halfB_in_ga(T74, s(s(T97))))
U6_gaga(T74, T97, T98, T100, halfB_out_ga(T74, s(s(T97)))) → U7_gaga(T74, T97, T98, T100, pC_in_gaga(T97, X228, s(T98), T100))
U7_gaga(T74, T97, T98, T100, pC_out_gaga(T97, X228, s(T98), T100)) → pC_out_gaga(T74, s(s(T97)), T98, T100)
U78_ga(T12, T76, pC_out_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76)) → log2D_out_ga(s(s(T12)), T76)

The argument filtering Pi contains the following mapping:
log2D_in_ga(x1, x2)  =  log2D_in_ga(x1)
0  =  0
log2D_out_ga(x1, x2)  =  log2D_out_ga
s(x1)  =  s(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
halfB_in_ga(x1, x2)  =  halfB_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
halfA_in_ga(x1, x2)  =  halfA_in_ga(x1)
halfA_out_ga(x1, x2)  =  halfA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
halfB_out_ga(x1, x2)  =  halfB_out_ga(x2)
U9_ga(x1, x2)  =  U9_ga(x2)
halfB_in_gg(x1, x2)  =  halfB_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
halfA_in_gg(x1, x2)  =  halfA_in_gg(x1, x2)
halfA_out_gg(x1, x2)  =  halfA_out_gg
U1_gg(x1, x2, x3)  =  U1_gg(x3)
halfB_out_gg(x1, x2)  =  halfB_out_gg
U10_ga(x1, x2)  =  U10_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2)  =  U13_ga(x2)
U14_ga(x1, x2)  =  U14_ga(x2)
U15_ga(x1, x2)  =  U15_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
U18_ga(x1, x2, x3)  =  U18_ga(x3)
U19_ga(x1, x2)  =  U19_ga(x2)
U20_ga(x1, x2)  =  U20_ga(x2)
U21_ga(x1, x2)  =  U21_ga(x2)
U22_ga(x1, x2)  =  U22_ga(x2)
U23_ga(x1, x2, x3)  =  U23_ga(x3)
U24_ga(x1, x2, x3)  =  U24_ga(x3)
U25_ga(x1, x2, x3)  =  U25_ga(x3)
U26_ga(x1, x2, x3)  =  U26_ga(x3)
U27_ga(x1, x2)  =  U27_ga(x2)
U28_ga(x1, x2)  =  U28_ga(x2)
U29_ga(x1, x2)  =  U29_ga(x2)
U30_ga(x1, x2)  =  U30_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U33_ga(x1, x2, x3)  =  U33_ga(x3)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
U35_ga(x1, x2, x3)  =  U35_ga(x3)
U36_ga(x1, x2, x3)  =  U36_ga(x3)
U37_ga(x1, x2)  =  U37_ga(x2)
U38_ga(x1, x2)  =  U38_ga(x2)
U39_ga(x1, x2)  =  U39_ga(x2)
U40_ga(x1, x2)  =  U40_ga(x2)
U41_ga(x1, x2)  =  U41_ga(x2)
U42_ga(x1, x2)  =  U42_ga(x2)
U43_ga(x1, x2, x3)  =  U43_ga(x3)
U44_ga(x1, x2, x3)  =  U44_ga(x3)
U45_ga(x1, x2, x3)  =  U45_ga(x3)
U46_ga(x1, x2, x3)  =  U46_ga(x3)
U47_ga(x1, x2, x3)  =  U47_ga(x3)
U48_ga(x1, x2, x3)  =  U48_ga(x3)
U49_ga(x1, x2)  =  U49_ga(x2)
U50_ga(x1, x2)  =  U50_ga(x2)
U51_ga(x1, x2)  =  U51_ga(x2)
U52_ga(x1, x2)  =  U52_ga(x2)
U53_ga(x1, x2)  =  U53_ga(x2)
U54_ga(x1, x2)  =  U54_ga(x2)
U55_ga(x1, x2)  =  U55_ga(x2)
U56_ga(x1, x2, x3)  =  U56_ga(x3)
U57_ga(x1, x2, x3)  =  U57_ga(x3)
U58_ga(x1, x2, x3)  =  U58_ga(x3)
U59_ga(x1, x2, x3)  =  U59_ga(x3)
U60_ga(x1, x2, x3)  =  U60_ga(x3)
U61_ga(x1, x2, x3)  =  U61_ga(x3)
U62_ga(x1, x2, x3)  =  U62_ga(x3)
U63_ga(x1, x2)  =  U63_ga(x2)
U64_ga(x1, x2)  =  U64_ga(x2)
U65_ga(x1, x2)  =  U65_ga(x2)
U66_ga(x1, x2)  =  U66_ga(x2)
U67_ga(x1, x2)  =  U67_ga(x2)
U68_ga(x1, x2)  =  U68_ga(x2)
U69_ga(x1, x2)  =  U69_ga(x2)
U70_ga(x1, x2)  =  U70_ga(x2)
U71_ga(x1, x2, x3)  =  U71_ga(x3)
U72_ga(x1, x2, x3)  =  U72_ga(x3)
U73_ga(x1, x2, x3)  =  U73_ga(x3)
U74_ga(x1, x2, x3)  =  U74_ga(x3)
U75_ga(x1, x2, x3)  =  U75_ga(x3)
U76_ga(x1, x2, x3)  =  U76_ga(x3)
U77_ga(x1, x2, x3)  =  U77_ga(x3)
U78_ga(x1, x2, x3)  =  U78_ga(x3)
pC_in_gaga(x1, x2, x3, x4)  =  pC_in_gaga(x1, x3)
U3_gaga(x1, x2, x3, x4, x5)  =  U3_gaga(x5)
pC_out_gaga(x1, x2, x3, x4)  =  pC_out_gaga(x2)
U4_gaga(x1, x2, x3)  =  U4_gaga(x3)
U5_gaga(x1, x2, x3)  =  U5_gaga(x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x3, x5)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x2, x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

log2D_in_ga(0, 0) → log2D_out_ga(0, 0)
log2D_in_ga(s(0), 0) → log2D_out_ga(s(0), 0)
log2D_in_ga(s(s(T12)), T14) → U8_ga(T12, T14, halfB_in_ga(T12, X26))
halfB_in_ga(T18, s(X35)) → U2_ga(T18, X35, halfA_in_ga(T18, X35))
halfA_in_ga(0, 0) → halfA_out_ga(0, 0)
halfA_in_ga(s(0), 0) → halfA_out_ga(s(0), 0)
halfA_in_ga(s(s(T21)), s(X44)) → U1_ga(T21, X44, halfA_in_ga(T21, X44))
U1_ga(T21, X44, halfA_out_ga(T21, X44)) → halfA_out_ga(s(s(T21)), s(X44))
U2_ga(T18, X35, halfA_out_ga(T18, X35)) → halfB_out_ga(T18, s(X35))
U8_ga(T12, T14, halfB_out_ga(T12, X26)) → log2D_out_ga(s(s(T12)), T14)
log2D_in_ga(s(s(T12)), s(0)) → U9_ga(T12, halfB_in_gg(T12, 0))
halfB_in_gg(T18, s(X35)) → U2_gg(T18, X35, halfA_in_gg(T18, X35))
halfA_in_gg(0, 0) → halfA_out_gg(0, 0)
halfA_in_gg(s(0), 0) → halfA_out_gg(s(0), 0)
halfA_in_gg(s(s(T21)), s(X44)) → U1_gg(T21, X44, halfA_in_gg(T21, X44))
U1_gg(T21, X44, halfA_out_gg(T21, X44)) → halfA_out_gg(s(s(T21)), s(X44))
U2_gg(T18, X35, halfA_out_gg(T18, X35)) → halfB_out_gg(T18, s(X35))
U9_ga(T12, halfB_out_gg(T12, 0)) → log2D_out_ga(s(s(T12)), s(0))
log2D_in_ga(s(s(T12)), s(0)) → U10_ga(T12, halfB_in_gg(T12, s(0)))
U10_ga(T12, halfB_out_gg(T12, s(0))) → log2D_out_ga(s(s(T12)), s(0))
log2D_in_ga(s(s(T12)), T28) → U11_ga(T12, T28, halfB_in_ga(T12, s(s(T26))))
U11_ga(T12, T28, halfB_out_ga(T12, s(s(T26)))) → U12_ga(T12, T28, halfB_in_ga(T26, X67))
U12_ga(T12, T28, halfB_out_ga(T26, X67)) → log2D_out_ga(s(s(T12)), T28)
log2D_in_ga(s(s(T12)), s(s(0))) → U13_ga(T12, halfB_in_ga(T12, s(s(T26))))
U13_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U14_ga(T12, halfB_in_gg(T26, 0))
U14_ga(T12, halfB_out_gg(T26, 0)) → log2D_out_ga(s(s(T12)), s(s(0)))
U13_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U15_ga(T12, halfB_in_gg(T26, s(0)))
U15_ga(T12, halfB_out_gg(T26, s(0))) → log2D_out_ga(s(s(T12)), s(s(0)))
log2D_in_ga(s(s(T12)), T36) → U16_ga(T12, T36, halfB_in_ga(T12, s(s(T26))))
U16_ga(T12, T36, halfB_out_ga(T12, s(s(T26)))) → U17_ga(T12, T36, halfB_in_ga(T26, s(s(T34))))
U17_ga(T12, T36, halfB_out_ga(T26, s(s(T34)))) → U18_ga(T12, T36, halfB_in_ga(T34, X90))
U18_ga(T12, T36, halfB_out_ga(T34, X90)) → log2D_out_ga(s(s(T12)), T36)
log2D_in_ga(s(s(T12)), s(s(s(0)))) → U19_ga(T12, halfB_in_ga(T12, s(s(T26))))
U19_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U20_ga(T12, halfB_in_ga(T26, s(s(T34))))
U20_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U21_ga(T12, halfB_in_gg(T34, 0))
U21_ga(T12, halfB_out_gg(T34, 0)) → log2D_out_ga(s(s(T12)), s(s(s(0))))
U20_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U22_ga(T12, halfB_in_gg(T34, s(0)))
U22_ga(T12, halfB_out_gg(T34, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(0))))
log2D_in_ga(s(s(T12)), T44) → U23_ga(T12, T44, halfB_in_ga(T12, s(s(T26))))
U23_ga(T12, T44, halfB_out_ga(T12, s(s(T26)))) → U24_ga(T12, T44, halfB_in_ga(T26, s(s(T34))))
U24_ga(T12, T44, halfB_out_ga(T26, s(s(T34)))) → U25_ga(T12, T44, halfB_in_ga(T34, s(s(T42))))
U25_ga(T12, T44, halfB_out_ga(T34, s(s(T42)))) → U26_ga(T12, T44, halfB_in_ga(T42, X113))
U26_ga(T12, T44, halfB_out_ga(T42, X113)) → log2D_out_ga(s(s(T12)), T44)
log2D_in_ga(s(s(T12)), s(s(s(s(0))))) → U27_ga(T12, halfB_in_ga(T12, s(s(T26))))
U27_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U28_ga(T12, halfB_in_ga(T26, s(s(T34))))
U28_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U29_ga(T12, halfB_in_ga(T34, s(s(T42))))
U29_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U30_ga(T12, halfB_in_gg(T42, 0))
U30_ga(T12, halfB_out_gg(T42, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(0)))))
U29_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U31_ga(T12, halfB_in_gg(T42, s(0)))
U31_ga(T12, halfB_out_gg(T42, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(0)))))
log2D_in_ga(s(s(T12)), T52) → U32_ga(T12, T52, halfB_in_ga(T12, s(s(T26))))
U32_ga(T12, T52, halfB_out_ga(T12, s(s(T26)))) → U33_ga(T12, T52, halfB_in_ga(T26, s(s(T34))))
U33_ga(T12, T52, halfB_out_ga(T26, s(s(T34)))) → U34_ga(T12, T52, halfB_in_ga(T34, s(s(T42))))
U34_ga(T12, T52, halfB_out_ga(T34, s(s(T42)))) → U35_ga(T12, T52, halfB_in_ga(T42, s(s(T50))))
U35_ga(T12, T52, halfB_out_ga(T42, s(s(T50)))) → U36_ga(T12, T52, halfB_in_ga(T50, X136))
U36_ga(T12, T52, halfB_out_ga(T50, X136)) → log2D_out_ga(s(s(T12)), T52)
log2D_in_ga(s(s(T12)), s(s(s(s(s(0)))))) → U37_ga(T12, halfB_in_ga(T12, s(s(T26))))
U37_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U38_ga(T12, halfB_in_ga(T26, s(s(T34))))
U38_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U39_ga(T12, halfB_in_ga(T34, s(s(T42))))
U39_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U40_ga(T12, halfB_in_ga(T42, s(s(T50))))
U40_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U41_ga(T12, halfB_in_gg(T50, 0))
U41_ga(T12, halfB_out_gg(T50, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(0))))))
U40_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U42_ga(T12, halfB_in_gg(T50, s(0)))
U42_ga(T12, halfB_out_gg(T50, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(0))))))
log2D_in_ga(s(s(T12)), T60) → U43_ga(T12, T60, halfB_in_ga(T12, s(s(T26))))
U43_ga(T12, T60, halfB_out_ga(T12, s(s(T26)))) → U44_ga(T12, T60, halfB_in_ga(T26, s(s(T34))))
U44_ga(T12, T60, halfB_out_ga(T26, s(s(T34)))) → U45_ga(T12, T60, halfB_in_ga(T34, s(s(T42))))
U45_ga(T12, T60, halfB_out_ga(T34, s(s(T42)))) → U46_ga(T12, T60, halfB_in_ga(T42, s(s(T50))))
U46_ga(T12, T60, halfB_out_ga(T42, s(s(T50)))) → U47_ga(T12, T60, halfB_in_ga(T50, s(s(T58))))
U47_ga(T12, T60, halfB_out_ga(T50, s(s(T58)))) → U48_ga(T12, T60, halfB_in_ga(T58, X159))
U48_ga(T12, T60, halfB_out_ga(T58, X159)) → log2D_out_ga(s(s(T12)), T60)
log2D_in_ga(s(s(T12)), s(s(s(s(s(s(0))))))) → U49_ga(T12, halfB_in_ga(T12, s(s(T26))))
U49_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U50_ga(T12, halfB_in_ga(T26, s(s(T34))))
U50_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U51_ga(T12, halfB_in_ga(T34, s(s(T42))))
U51_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U52_ga(T12, halfB_in_ga(T42, s(s(T50))))
U52_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U53_ga(T12, halfB_in_ga(T50, s(s(T58))))
U53_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U54_ga(T12, halfB_in_gg(T58, 0))
U54_ga(T12, halfB_out_gg(T58, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
U53_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U55_ga(T12, halfB_in_gg(T58, s(0)))
U55_ga(T12, halfB_out_gg(T58, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
log2D_in_ga(s(s(T12)), T68) → U56_ga(T12, T68, halfB_in_ga(T12, s(s(T26))))
U56_ga(T12, T68, halfB_out_ga(T12, s(s(T26)))) → U57_ga(T12, T68, halfB_in_ga(T26, s(s(T34))))
U57_ga(T12, T68, halfB_out_ga(T26, s(s(T34)))) → U58_ga(T12, T68, halfB_in_ga(T34, s(s(T42))))
U58_ga(T12, T68, halfB_out_ga(T34, s(s(T42)))) → U59_ga(T12, T68, halfB_in_ga(T42, s(s(T50))))
U59_ga(T12, T68, halfB_out_ga(T42, s(s(T50)))) → U60_ga(T12, T68, halfB_in_ga(T50, s(s(T58))))
U60_ga(T12, T68, halfB_out_ga(T50, s(s(T58)))) → U61_ga(T12, T68, halfB_in_ga(T58, s(s(T66))))
U61_ga(T12, T68, halfB_out_ga(T58, s(s(T66)))) → U62_ga(T12, T68, halfB_in_ga(T66, X182))
U62_ga(T12, T68, halfB_out_ga(T66, X182)) → log2D_out_ga(s(s(T12)), T68)
log2D_in_ga(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → U63_ga(T12, halfB_in_ga(T12, s(s(T26))))
U63_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U64_ga(T12, halfB_in_ga(T26, s(s(T34))))
U64_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U65_ga(T12, halfB_in_ga(T34, s(s(T42))))
U65_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U66_ga(T12, halfB_in_ga(T42, s(s(T50))))
U66_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U67_ga(T12, halfB_in_ga(T50, s(s(T58))))
U67_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U68_ga(T12, halfB_in_ga(T58, s(s(T66))))
U68_ga(T12, halfB_out_ga(T58, s(s(T66)))) → U69_ga(T12, halfB_in_gg(T66, 0))
U69_ga(T12, halfB_out_gg(T66, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
U68_ga(T12, halfB_out_ga(T58, s(s(T66)))) → U70_ga(T12, halfB_in_gg(T66, s(0)))
U70_ga(T12, halfB_out_gg(T66, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
log2D_in_ga(s(s(T12)), T76) → U71_ga(T12, T76, halfB_in_ga(T12, s(s(T26))))
U71_ga(T12, T76, halfB_out_ga(T12, s(s(T26)))) → U72_ga(T12, T76, halfB_in_ga(T26, s(s(T34))))
U72_ga(T12, T76, halfB_out_ga(T26, s(s(T34)))) → U73_ga(T12, T76, halfB_in_ga(T34, s(s(T42))))
U73_ga(T12, T76, halfB_out_ga(T34, s(s(T42)))) → U74_ga(T12, T76, halfB_in_ga(T42, s(s(T50))))
U74_ga(T12, T76, halfB_out_ga(T42, s(s(T50)))) → U75_ga(T12, T76, halfB_in_ga(T50, s(s(T58))))
U75_ga(T12, T76, halfB_out_ga(T50, s(s(T58)))) → U76_ga(T12, T76, halfB_in_ga(T58, s(s(T66))))
U76_ga(T12, T76, halfB_out_ga(T58, s(s(T66)))) → U77_ga(T12, T76, halfB_in_ga(T66, s(s(T74))))
U77_ga(T12, T76, halfB_out_ga(T66, s(s(T74)))) → U78_ga(T12, T76, pC_in_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76))
pC_in_gaga(T74, X205, T77, T76) → U3_gaga(T74, X205, T77, T76, halfB_in_ga(T74, X205))
U3_gaga(T74, X205, T77, T76, halfB_out_ga(T74, X205)) → pC_out_gaga(T74, X205, T77, T76)
pC_in_gaga(T74, 0, T85, s(T85)) → U4_gaga(T74, T85, halfB_in_gg(T74, 0))
U4_gaga(T74, T85, halfB_out_gg(T74, 0)) → pC_out_gaga(T74, 0, T85, s(T85))
pC_in_gaga(T74, s(0), T90, s(T90)) → U5_gaga(T74, T90, halfB_in_gg(T74, s(0)))
U5_gaga(T74, T90, halfB_out_gg(T74, s(0))) → pC_out_gaga(T74, s(0), T90, s(T90))
pC_in_gaga(T74, s(s(T97)), T98, T100) → U6_gaga(T74, T97, T98, T100, halfB_in_ga(T74, s(s(T97))))
U6_gaga(T74, T97, T98, T100, halfB_out_ga(T74, s(s(T97)))) → U7_gaga(T74, T97, T98, T100, pC_in_gaga(T97, X228, s(T98), T100))
U7_gaga(T74, T97, T98, T100, pC_out_gaga(T97, X228, s(T98), T100)) → pC_out_gaga(T74, s(s(T97)), T98, T100)
U78_ga(T12, T76, pC_out_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76)) → log2D_out_ga(s(s(T12)), T76)

The argument filtering Pi contains the following mapping:
log2D_in_ga(x1, x2)  =  log2D_in_ga(x1)
0  =  0
log2D_out_ga(x1, x2)  =  log2D_out_ga
s(x1)  =  s(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
halfB_in_ga(x1, x2)  =  halfB_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
halfA_in_ga(x1, x2)  =  halfA_in_ga(x1)
halfA_out_ga(x1, x2)  =  halfA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
halfB_out_ga(x1, x2)  =  halfB_out_ga(x2)
U9_ga(x1, x2)  =  U9_ga(x2)
halfB_in_gg(x1, x2)  =  halfB_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
halfA_in_gg(x1, x2)  =  halfA_in_gg(x1, x2)
halfA_out_gg(x1, x2)  =  halfA_out_gg
U1_gg(x1, x2, x3)  =  U1_gg(x3)
halfB_out_gg(x1, x2)  =  halfB_out_gg
U10_ga(x1, x2)  =  U10_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2)  =  U13_ga(x2)
U14_ga(x1, x2)  =  U14_ga(x2)
U15_ga(x1, x2)  =  U15_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
U18_ga(x1, x2, x3)  =  U18_ga(x3)
U19_ga(x1, x2)  =  U19_ga(x2)
U20_ga(x1, x2)  =  U20_ga(x2)
U21_ga(x1, x2)  =  U21_ga(x2)
U22_ga(x1, x2)  =  U22_ga(x2)
U23_ga(x1, x2, x3)  =  U23_ga(x3)
U24_ga(x1, x2, x3)  =  U24_ga(x3)
U25_ga(x1, x2, x3)  =  U25_ga(x3)
U26_ga(x1, x2, x3)  =  U26_ga(x3)
U27_ga(x1, x2)  =  U27_ga(x2)
U28_ga(x1, x2)  =  U28_ga(x2)
U29_ga(x1, x2)  =  U29_ga(x2)
U30_ga(x1, x2)  =  U30_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U33_ga(x1, x2, x3)  =  U33_ga(x3)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
U35_ga(x1, x2, x3)  =  U35_ga(x3)
U36_ga(x1, x2, x3)  =  U36_ga(x3)
U37_ga(x1, x2)  =  U37_ga(x2)
U38_ga(x1, x2)  =  U38_ga(x2)
U39_ga(x1, x2)  =  U39_ga(x2)
U40_ga(x1, x2)  =  U40_ga(x2)
U41_ga(x1, x2)  =  U41_ga(x2)
U42_ga(x1, x2)  =  U42_ga(x2)
U43_ga(x1, x2, x3)  =  U43_ga(x3)
U44_ga(x1, x2, x3)  =  U44_ga(x3)
U45_ga(x1, x2, x3)  =  U45_ga(x3)
U46_ga(x1, x2, x3)  =  U46_ga(x3)
U47_ga(x1, x2, x3)  =  U47_ga(x3)
U48_ga(x1, x2, x3)  =  U48_ga(x3)
U49_ga(x1, x2)  =  U49_ga(x2)
U50_ga(x1, x2)  =  U50_ga(x2)
U51_ga(x1, x2)  =  U51_ga(x2)
U52_ga(x1, x2)  =  U52_ga(x2)
U53_ga(x1, x2)  =  U53_ga(x2)
U54_ga(x1, x2)  =  U54_ga(x2)
U55_ga(x1, x2)  =  U55_ga(x2)
U56_ga(x1, x2, x3)  =  U56_ga(x3)
U57_ga(x1, x2, x3)  =  U57_ga(x3)
U58_ga(x1, x2, x3)  =  U58_ga(x3)
U59_ga(x1, x2, x3)  =  U59_ga(x3)
U60_ga(x1, x2, x3)  =  U60_ga(x3)
U61_ga(x1, x2, x3)  =  U61_ga(x3)
U62_ga(x1, x2, x3)  =  U62_ga(x3)
U63_ga(x1, x2)  =  U63_ga(x2)
U64_ga(x1, x2)  =  U64_ga(x2)
U65_ga(x1, x2)  =  U65_ga(x2)
U66_ga(x1, x2)  =  U66_ga(x2)
U67_ga(x1, x2)  =  U67_ga(x2)
U68_ga(x1, x2)  =  U68_ga(x2)
U69_ga(x1, x2)  =  U69_ga(x2)
U70_ga(x1, x2)  =  U70_ga(x2)
U71_ga(x1, x2, x3)  =  U71_ga(x3)
U72_ga(x1, x2, x3)  =  U72_ga(x3)
U73_ga(x1, x2, x3)  =  U73_ga(x3)
U74_ga(x1, x2, x3)  =  U74_ga(x3)
U75_ga(x1, x2, x3)  =  U75_ga(x3)
U76_ga(x1, x2, x3)  =  U76_ga(x3)
U77_ga(x1, x2, x3)  =  U77_ga(x3)
U78_ga(x1, x2, x3)  =  U78_ga(x3)
pC_in_gaga(x1, x2, x3, x4)  =  pC_in_gaga(x1, x3)
U3_gaga(x1, x2, x3, x4, x5)  =  U3_gaga(x5)
pC_out_gaga(x1, x2, x3, x4)  =  pC_out_gaga(x2)
U4_gaga(x1, x2, x3)  =  U4_gaga(x3)
U5_gaga(x1, x2, x3)  =  U5_gaga(x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x3, x5)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x2, x5)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

LOG2D_IN_GA(s(s(T12)), T14) → U8_GA(T12, T14, halfB_in_ga(T12, X26))
LOG2D_IN_GA(s(s(T12)), T14) → HALFB_IN_GA(T12, X26)
HALFB_IN_GA(T18, s(X35)) → U2_GA(T18, X35, halfA_in_ga(T18, X35))
HALFB_IN_GA(T18, s(X35)) → HALFA_IN_GA(T18, X35)
HALFA_IN_GA(s(s(T21)), s(X44)) → U1_GA(T21, X44, halfA_in_ga(T21, X44))
HALFA_IN_GA(s(s(T21)), s(X44)) → HALFA_IN_GA(T21, X44)
LOG2D_IN_GA(s(s(T12)), s(0)) → U9_GA(T12, halfB_in_gg(T12, 0))
LOG2D_IN_GA(s(s(T12)), s(0)) → HALFB_IN_GG(T12, 0)
HALFB_IN_GG(T18, s(X35)) → U2_GG(T18, X35, halfA_in_gg(T18, X35))
HALFB_IN_GG(T18, s(X35)) → HALFA_IN_GG(T18, X35)
HALFA_IN_GG(s(s(T21)), s(X44)) → U1_GG(T21, X44, halfA_in_gg(T21, X44))
HALFA_IN_GG(s(s(T21)), s(X44)) → HALFA_IN_GG(T21, X44)
LOG2D_IN_GA(s(s(T12)), s(0)) → U10_GA(T12, halfB_in_gg(T12, s(0)))
LOG2D_IN_GA(s(s(T12)), s(0)) → HALFB_IN_GG(T12, s(0))
LOG2D_IN_GA(s(s(T12)), T28) → U11_GA(T12, T28, halfB_in_ga(T12, s(s(T26))))
LOG2D_IN_GA(s(s(T12)), T28) → HALFB_IN_GA(T12, s(s(T26)))
U11_GA(T12, T28, halfB_out_ga(T12, s(s(T26)))) → U12_GA(T12, T28, halfB_in_ga(T26, X67))
U11_GA(T12, T28, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, X67)
LOG2D_IN_GA(s(s(T12)), s(s(0))) → U13_GA(T12, halfB_in_ga(T12, s(s(T26))))
LOG2D_IN_GA(s(s(T12)), s(s(0))) → HALFB_IN_GA(T12, s(s(T26)))
U13_GA(T12, halfB_out_ga(T12, s(s(T26)))) → U14_GA(T12, halfB_in_gg(T26, 0))
U13_GA(T12, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GG(T26, 0)
U13_GA(T12, halfB_out_ga(T12, s(s(T26)))) → U15_GA(T12, halfB_in_gg(T26, s(0)))
U13_GA(T12, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GG(T26, s(0))
LOG2D_IN_GA(s(s(T12)), T36) → U16_GA(T12, T36, halfB_in_ga(T12, s(s(T26))))
U16_GA(T12, T36, halfB_out_ga(T12, s(s(T26)))) → U17_GA(T12, T36, halfB_in_ga(T26, s(s(T34))))
U16_GA(T12, T36, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U17_GA(T12, T36, halfB_out_ga(T26, s(s(T34)))) → U18_GA(T12, T36, halfB_in_ga(T34, X90))
U17_GA(T12, T36, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, X90)
LOG2D_IN_GA(s(s(T12)), s(s(s(0)))) → U19_GA(T12, halfB_in_ga(T12, s(s(T26))))
LOG2D_IN_GA(s(s(T12)), s(s(s(0)))) → HALFB_IN_GA(T12, s(s(T26)))
U19_GA(T12, halfB_out_ga(T12, s(s(T26)))) → U20_GA(T12, halfB_in_ga(T26, s(s(T34))))
U19_GA(T12, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U20_GA(T12, halfB_out_ga(T26, s(s(T34)))) → U21_GA(T12, halfB_in_gg(T34, 0))
U20_GA(T12, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GG(T34, 0)
U20_GA(T12, halfB_out_ga(T26, s(s(T34)))) → U22_GA(T12, halfB_in_gg(T34, s(0)))
U20_GA(T12, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GG(T34, s(0))
LOG2D_IN_GA(s(s(T12)), T44) → U23_GA(T12, T44, halfB_in_ga(T12, s(s(T26))))
U23_GA(T12, T44, halfB_out_ga(T12, s(s(T26)))) → U24_GA(T12, T44, halfB_in_ga(T26, s(s(T34))))
U23_GA(T12, T44, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U24_GA(T12, T44, halfB_out_ga(T26, s(s(T34)))) → U25_GA(T12, T44, halfB_in_ga(T34, s(s(T42))))
U24_GA(T12, T44, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, s(s(T42)))
U25_GA(T12, T44, halfB_out_ga(T34, s(s(T42)))) → U26_GA(T12, T44, halfB_in_ga(T42, X113))
U25_GA(T12, T44, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GA(T42, X113)
LOG2D_IN_GA(s(s(T12)), s(s(s(s(0))))) → U27_GA(T12, halfB_in_ga(T12, s(s(T26))))
LOG2D_IN_GA(s(s(T12)), s(s(s(s(0))))) → HALFB_IN_GA(T12, s(s(T26)))
U27_GA(T12, halfB_out_ga(T12, s(s(T26)))) → U28_GA(T12, halfB_in_ga(T26, s(s(T34))))
U27_GA(T12, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U28_GA(T12, halfB_out_ga(T26, s(s(T34)))) → U29_GA(T12, halfB_in_ga(T34, s(s(T42))))
U28_GA(T12, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, s(s(T42)))
U29_GA(T12, halfB_out_ga(T34, s(s(T42)))) → U30_GA(T12, halfB_in_gg(T42, 0))
U29_GA(T12, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GG(T42, 0)
U29_GA(T12, halfB_out_ga(T34, s(s(T42)))) → U31_GA(T12, halfB_in_gg(T42, s(0)))
U29_GA(T12, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GG(T42, s(0))
LOG2D_IN_GA(s(s(T12)), T52) → U32_GA(T12, T52, halfB_in_ga(T12, s(s(T26))))
U32_GA(T12, T52, halfB_out_ga(T12, s(s(T26)))) → U33_GA(T12, T52, halfB_in_ga(T26, s(s(T34))))
U32_GA(T12, T52, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U33_GA(T12, T52, halfB_out_ga(T26, s(s(T34)))) → U34_GA(T12, T52, halfB_in_ga(T34, s(s(T42))))
U33_GA(T12, T52, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, s(s(T42)))
U34_GA(T12, T52, halfB_out_ga(T34, s(s(T42)))) → U35_GA(T12, T52, halfB_in_ga(T42, s(s(T50))))
U34_GA(T12, T52, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GA(T42, s(s(T50)))
U35_GA(T12, T52, halfB_out_ga(T42, s(s(T50)))) → U36_GA(T12, T52, halfB_in_ga(T50, X136))
U35_GA(T12, T52, halfB_out_ga(T42, s(s(T50)))) → HALFB_IN_GA(T50, X136)
LOG2D_IN_GA(s(s(T12)), s(s(s(s(s(0)))))) → U37_GA(T12, halfB_in_ga(T12, s(s(T26))))
LOG2D_IN_GA(s(s(T12)), s(s(s(s(s(0)))))) → HALFB_IN_GA(T12, s(s(T26)))
U37_GA(T12, halfB_out_ga(T12, s(s(T26)))) → U38_GA(T12, halfB_in_ga(T26, s(s(T34))))
U37_GA(T12, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U38_GA(T12, halfB_out_ga(T26, s(s(T34)))) → U39_GA(T12, halfB_in_ga(T34, s(s(T42))))
U38_GA(T12, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, s(s(T42)))
U39_GA(T12, halfB_out_ga(T34, s(s(T42)))) → U40_GA(T12, halfB_in_ga(T42, s(s(T50))))
U39_GA(T12, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GA(T42, s(s(T50)))
U40_GA(T12, halfB_out_ga(T42, s(s(T50)))) → U41_GA(T12, halfB_in_gg(T50, 0))
U40_GA(T12, halfB_out_ga(T42, s(s(T50)))) → HALFB_IN_GG(T50, 0)
U40_GA(T12, halfB_out_ga(T42, s(s(T50)))) → U42_GA(T12, halfB_in_gg(T50, s(0)))
U40_GA(T12, halfB_out_ga(T42, s(s(T50)))) → HALFB_IN_GG(T50, s(0))
LOG2D_IN_GA(s(s(T12)), T60) → U43_GA(T12, T60, halfB_in_ga(T12, s(s(T26))))
U43_GA(T12, T60, halfB_out_ga(T12, s(s(T26)))) → U44_GA(T12, T60, halfB_in_ga(T26, s(s(T34))))
U43_GA(T12, T60, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U44_GA(T12, T60, halfB_out_ga(T26, s(s(T34)))) → U45_GA(T12, T60, halfB_in_ga(T34, s(s(T42))))
U44_GA(T12, T60, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, s(s(T42)))
U45_GA(T12, T60, halfB_out_ga(T34, s(s(T42)))) → U46_GA(T12, T60, halfB_in_ga(T42, s(s(T50))))
U45_GA(T12, T60, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GA(T42, s(s(T50)))
U46_GA(T12, T60, halfB_out_ga(T42, s(s(T50)))) → U47_GA(T12, T60, halfB_in_ga(T50, s(s(T58))))
U46_GA(T12, T60, halfB_out_ga(T42, s(s(T50)))) → HALFB_IN_GA(T50, s(s(T58)))
U47_GA(T12, T60, halfB_out_ga(T50, s(s(T58)))) → U48_GA(T12, T60, halfB_in_ga(T58, X159))
U47_GA(T12, T60, halfB_out_ga(T50, s(s(T58)))) → HALFB_IN_GA(T58, X159)
LOG2D_IN_GA(s(s(T12)), s(s(s(s(s(s(0))))))) → U49_GA(T12, halfB_in_ga(T12, s(s(T26))))
LOG2D_IN_GA(s(s(T12)), s(s(s(s(s(s(0))))))) → HALFB_IN_GA(T12, s(s(T26)))
U49_GA(T12, halfB_out_ga(T12, s(s(T26)))) → U50_GA(T12, halfB_in_ga(T26, s(s(T34))))
U49_GA(T12, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U50_GA(T12, halfB_out_ga(T26, s(s(T34)))) → U51_GA(T12, halfB_in_ga(T34, s(s(T42))))
U50_GA(T12, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, s(s(T42)))
U51_GA(T12, halfB_out_ga(T34, s(s(T42)))) → U52_GA(T12, halfB_in_ga(T42, s(s(T50))))
U51_GA(T12, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GA(T42, s(s(T50)))
U52_GA(T12, halfB_out_ga(T42, s(s(T50)))) → U53_GA(T12, halfB_in_ga(T50, s(s(T58))))
U52_GA(T12, halfB_out_ga(T42, s(s(T50)))) → HALFB_IN_GA(T50, s(s(T58)))
U53_GA(T12, halfB_out_ga(T50, s(s(T58)))) → U54_GA(T12, halfB_in_gg(T58, 0))
U53_GA(T12, halfB_out_ga(T50, s(s(T58)))) → HALFB_IN_GG(T58, 0)
U53_GA(T12, halfB_out_ga(T50, s(s(T58)))) → U55_GA(T12, halfB_in_gg(T58, s(0)))
U53_GA(T12, halfB_out_ga(T50, s(s(T58)))) → HALFB_IN_GG(T58, s(0))
LOG2D_IN_GA(s(s(T12)), T68) → U56_GA(T12, T68, halfB_in_ga(T12, s(s(T26))))
U56_GA(T12, T68, halfB_out_ga(T12, s(s(T26)))) → U57_GA(T12, T68, halfB_in_ga(T26, s(s(T34))))
U56_GA(T12, T68, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U57_GA(T12, T68, halfB_out_ga(T26, s(s(T34)))) → U58_GA(T12, T68, halfB_in_ga(T34, s(s(T42))))
U57_GA(T12, T68, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, s(s(T42)))
U58_GA(T12, T68, halfB_out_ga(T34, s(s(T42)))) → U59_GA(T12, T68, halfB_in_ga(T42, s(s(T50))))
U58_GA(T12, T68, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GA(T42, s(s(T50)))
U59_GA(T12, T68, halfB_out_ga(T42, s(s(T50)))) → U60_GA(T12, T68, halfB_in_ga(T50, s(s(T58))))
U59_GA(T12, T68, halfB_out_ga(T42, s(s(T50)))) → HALFB_IN_GA(T50, s(s(T58)))
U60_GA(T12, T68, halfB_out_ga(T50, s(s(T58)))) → U61_GA(T12, T68, halfB_in_ga(T58, s(s(T66))))
U60_GA(T12, T68, halfB_out_ga(T50, s(s(T58)))) → HALFB_IN_GA(T58, s(s(T66)))
U61_GA(T12, T68, halfB_out_ga(T58, s(s(T66)))) → U62_GA(T12, T68, halfB_in_ga(T66, X182))
U61_GA(T12, T68, halfB_out_ga(T58, s(s(T66)))) → HALFB_IN_GA(T66, X182)
LOG2D_IN_GA(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → U63_GA(T12, halfB_in_ga(T12, s(s(T26))))
LOG2D_IN_GA(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → HALFB_IN_GA(T12, s(s(T26)))
U63_GA(T12, halfB_out_ga(T12, s(s(T26)))) → U64_GA(T12, halfB_in_ga(T26, s(s(T34))))
U63_GA(T12, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U64_GA(T12, halfB_out_ga(T26, s(s(T34)))) → U65_GA(T12, halfB_in_ga(T34, s(s(T42))))
U64_GA(T12, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, s(s(T42)))
U65_GA(T12, halfB_out_ga(T34, s(s(T42)))) → U66_GA(T12, halfB_in_ga(T42, s(s(T50))))
U65_GA(T12, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GA(T42, s(s(T50)))
U66_GA(T12, halfB_out_ga(T42, s(s(T50)))) → U67_GA(T12, halfB_in_ga(T50, s(s(T58))))
U66_GA(T12, halfB_out_ga(T42, s(s(T50)))) → HALFB_IN_GA(T50, s(s(T58)))
U67_GA(T12, halfB_out_ga(T50, s(s(T58)))) → U68_GA(T12, halfB_in_ga(T58, s(s(T66))))
U67_GA(T12, halfB_out_ga(T50, s(s(T58)))) → HALFB_IN_GA(T58, s(s(T66)))
U68_GA(T12, halfB_out_ga(T58, s(s(T66)))) → U69_GA(T12, halfB_in_gg(T66, 0))
U68_GA(T12, halfB_out_ga(T58, s(s(T66)))) → HALFB_IN_GG(T66, 0)
U68_GA(T12, halfB_out_ga(T58, s(s(T66)))) → U70_GA(T12, halfB_in_gg(T66, s(0)))
U68_GA(T12, halfB_out_ga(T58, s(s(T66)))) → HALFB_IN_GG(T66, s(0))
LOG2D_IN_GA(s(s(T12)), T76) → U71_GA(T12, T76, halfB_in_ga(T12, s(s(T26))))
U71_GA(T12, T76, halfB_out_ga(T12, s(s(T26)))) → U72_GA(T12, T76, halfB_in_ga(T26, s(s(T34))))
U71_GA(T12, T76, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U72_GA(T12, T76, halfB_out_ga(T26, s(s(T34)))) → U73_GA(T12, T76, halfB_in_ga(T34, s(s(T42))))
U72_GA(T12, T76, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, s(s(T42)))
U73_GA(T12, T76, halfB_out_ga(T34, s(s(T42)))) → U74_GA(T12, T76, halfB_in_ga(T42, s(s(T50))))
U73_GA(T12, T76, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GA(T42, s(s(T50)))
U74_GA(T12, T76, halfB_out_ga(T42, s(s(T50)))) → U75_GA(T12, T76, halfB_in_ga(T50, s(s(T58))))
U74_GA(T12, T76, halfB_out_ga(T42, s(s(T50)))) → HALFB_IN_GA(T50, s(s(T58)))
U75_GA(T12, T76, halfB_out_ga(T50, s(s(T58)))) → U76_GA(T12, T76, halfB_in_ga(T58, s(s(T66))))
U75_GA(T12, T76, halfB_out_ga(T50, s(s(T58)))) → HALFB_IN_GA(T58, s(s(T66)))
U76_GA(T12, T76, halfB_out_ga(T58, s(s(T66)))) → U77_GA(T12, T76, halfB_in_ga(T66, s(s(T74))))
U76_GA(T12, T76, halfB_out_ga(T58, s(s(T66)))) → HALFB_IN_GA(T66, s(s(T74)))
U77_GA(T12, T76, halfB_out_ga(T66, s(s(T74)))) → U78_GA(T12, T76, pC_in_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76))
U77_GA(T12, T76, halfB_out_ga(T66, s(s(T74)))) → PC_IN_GAGA(T74, X205, s(s(s(s(s(s(s(0))))))), T76)
PC_IN_GAGA(T74, X205, T77, T76) → U3_GAGA(T74, X205, T77, T76, halfB_in_ga(T74, X205))
PC_IN_GAGA(T74, X205, T77, T76) → HALFB_IN_GA(T74, X205)
PC_IN_GAGA(T74, 0, T85, s(T85)) → U4_GAGA(T74, T85, halfB_in_gg(T74, 0))
PC_IN_GAGA(T74, 0, T85, s(T85)) → HALFB_IN_GG(T74, 0)
PC_IN_GAGA(T74, s(0), T90, s(T90)) → U5_GAGA(T74, T90, halfB_in_gg(T74, s(0)))
PC_IN_GAGA(T74, s(0), T90, s(T90)) → HALFB_IN_GG(T74, s(0))
PC_IN_GAGA(T74, s(s(T97)), T98, T100) → U6_GAGA(T74, T97, T98, T100, halfB_in_ga(T74, s(s(T97))))
PC_IN_GAGA(T74, s(s(T97)), T98, T100) → HALFB_IN_GA(T74, s(s(T97)))
U6_GAGA(T74, T97, T98, T100, halfB_out_ga(T74, s(s(T97)))) → U7_GAGA(T74, T97, T98, T100, pC_in_gaga(T97, X228, s(T98), T100))
U6_GAGA(T74, T97, T98, T100, halfB_out_ga(T74, s(s(T97)))) → PC_IN_GAGA(T97, X228, s(T98), T100)

The TRS R consists of the following rules:

log2D_in_ga(0, 0) → log2D_out_ga(0, 0)
log2D_in_ga(s(0), 0) → log2D_out_ga(s(0), 0)
log2D_in_ga(s(s(T12)), T14) → U8_ga(T12, T14, halfB_in_ga(T12, X26))
halfB_in_ga(T18, s(X35)) → U2_ga(T18, X35, halfA_in_ga(T18, X35))
halfA_in_ga(0, 0) → halfA_out_ga(0, 0)
halfA_in_ga(s(0), 0) → halfA_out_ga(s(0), 0)
halfA_in_ga(s(s(T21)), s(X44)) → U1_ga(T21, X44, halfA_in_ga(T21, X44))
U1_ga(T21, X44, halfA_out_ga(T21, X44)) → halfA_out_ga(s(s(T21)), s(X44))
U2_ga(T18, X35, halfA_out_ga(T18, X35)) → halfB_out_ga(T18, s(X35))
U8_ga(T12, T14, halfB_out_ga(T12, X26)) → log2D_out_ga(s(s(T12)), T14)
log2D_in_ga(s(s(T12)), s(0)) → U9_ga(T12, halfB_in_gg(T12, 0))
halfB_in_gg(T18, s(X35)) → U2_gg(T18, X35, halfA_in_gg(T18, X35))
halfA_in_gg(0, 0) → halfA_out_gg(0, 0)
halfA_in_gg(s(0), 0) → halfA_out_gg(s(0), 0)
halfA_in_gg(s(s(T21)), s(X44)) → U1_gg(T21, X44, halfA_in_gg(T21, X44))
U1_gg(T21, X44, halfA_out_gg(T21, X44)) → halfA_out_gg(s(s(T21)), s(X44))
U2_gg(T18, X35, halfA_out_gg(T18, X35)) → halfB_out_gg(T18, s(X35))
U9_ga(T12, halfB_out_gg(T12, 0)) → log2D_out_ga(s(s(T12)), s(0))
log2D_in_ga(s(s(T12)), s(0)) → U10_ga(T12, halfB_in_gg(T12, s(0)))
U10_ga(T12, halfB_out_gg(T12, s(0))) → log2D_out_ga(s(s(T12)), s(0))
log2D_in_ga(s(s(T12)), T28) → U11_ga(T12, T28, halfB_in_ga(T12, s(s(T26))))
U11_ga(T12, T28, halfB_out_ga(T12, s(s(T26)))) → U12_ga(T12, T28, halfB_in_ga(T26, X67))
U12_ga(T12, T28, halfB_out_ga(T26, X67)) → log2D_out_ga(s(s(T12)), T28)
log2D_in_ga(s(s(T12)), s(s(0))) → U13_ga(T12, halfB_in_ga(T12, s(s(T26))))
U13_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U14_ga(T12, halfB_in_gg(T26, 0))
U14_ga(T12, halfB_out_gg(T26, 0)) → log2D_out_ga(s(s(T12)), s(s(0)))
U13_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U15_ga(T12, halfB_in_gg(T26, s(0)))
U15_ga(T12, halfB_out_gg(T26, s(0))) → log2D_out_ga(s(s(T12)), s(s(0)))
log2D_in_ga(s(s(T12)), T36) → U16_ga(T12, T36, halfB_in_ga(T12, s(s(T26))))
U16_ga(T12, T36, halfB_out_ga(T12, s(s(T26)))) → U17_ga(T12, T36, halfB_in_ga(T26, s(s(T34))))
U17_ga(T12, T36, halfB_out_ga(T26, s(s(T34)))) → U18_ga(T12, T36, halfB_in_ga(T34, X90))
U18_ga(T12, T36, halfB_out_ga(T34, X90)) → log2D_out_ga(s(s(T12)), T36)
log2D_in_ga(s(s(T12)), s(s(s(0)))) → U19_ga(T12, halfB_in_ga(T12, s(s(T26))))
U19_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U20_ga(T12, halfB_in_ga(T26, s(s(T34))))
U20_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U21_ga(T12, halfB_in_gg(T34, 0))
U21_ga(T12, halfB_out_gg(T34, 0)) → log2D_out_ga(s(s(T12)), s(s(s(0))))
U20_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U22_ga(T12, halfB_in_gg(T34, s(0)))
U22_ga(T12, halfB_out_gg(T34, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(0))))
log2D_in_ga(s(s(T12)), T44) → U23_ga(T12, T44, halfB_in_ga(T12, s(s(T26))))
U23_ga(T12, T44, halfB_out_ga(T12, s(s(T26)))) → U24_ga(T12, T44, halfB_in_ga(T26, s(s(T34))))
U24_ga(T12, T44, halfB_out_ga(T26, s(s(T34)))) → U25_ga(T12, T44, halfB_in_ga(T34, s(s(T42))))
U25_ga(T12, T44, halfB_out_ga(T34, s(s(T42)))) → U26_ga(T12, T44, halfB_in_ga(T42, X113))
U26_ga(T12, T44, halfB_out_ga(T42, X113)) → log2D_out_ga(s(s(T12)), T44)
log2D_in_ga(s(s(T12)), s(s(s(s(0))))) → U27_ga(T12, halfB_in_ga(T12, s(s(T26))))
U27_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U28_ga(T12, halfB_in_ga(T26, s(s(T34))))
U28_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U29_ga(T12, halfB_in_ga(T34, s(s(T42))))
U29_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U30_ga(T12, halfB_in_gg(T42, 0))
U30_ga(T12, halfB_out_gg(T42, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(0)))))
U29_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U31_ga(T12, halfB_in_gg(T42, s(0)))
U31_ga(T12, halfB_out_gg(T42, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(0)))))
log2D_in_ga(s(s(T12)), T52) → U32_ga(T12, T52, halfB_in_ga(T12, s(s(T26))))
U32_ga(T12, T52, halfB_out_ga(T12, s(s(T26)))) → U33_ga(T12, T52, halfB_in_ga(T26, s(s(T34))))
U33_ga(T12, T52, halfB_out_ga(T26, s(s(T34)))) → U34_ga(T12, T52, halfB_in_ga(T34, s(s(T42))))
U34_ga(T12, T52, halfB_out_ga(T34, s(s(T42)))) → U35_ga(T12, T52, halfB_in_ga(T42, s(s(T50))))
U35_ga(T12, T52, halfB_out_ga(T42, s(s(T50)))) → U36_ga(T12, T52, halfB_in_ga(T50, X136))
U36_ga(T12, T52, halfB_out_ga(T50, X136)) → log2D_out_ga(s(s(T12)), T52)
log2D_in_ga(s(s(T12)), s(s(s(s(s(0)))))) → U37_ga(T12, halfB_in_ga(T12, s(s(T26))))
U37_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U38_ga(T12, halfB_in_ga(T26, s(s(T34))))
U38_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U39_ga(T12, halfB_in_ga(T34, s(s(T42))))
U39_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U40_ga(T12, halfB_in_ga(T42, s(s(T50))))
U40_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U41_ga(T12, halfB_in_gg(T50, 0))
U41_ga(T12, halfB_out_gg(T50, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(0))))))
U40_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U42_ga(T12, halfB_in_gg(T50, s(0)))
U42_ga(T12, halfB_out_gg(T50, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(0))))))
log2D_in_ga(s(s(T12)), T60) → U43_ga(T12, T60, halfB_in_ga(T12, s(s(T26))))
U43_ga(T12, T60, halfB_out_ga(T12, s(s(T26)))) → U44_ga(T12, T60, halfB_in_ga(T26, s(s(T34))))
U44_ga(T12, T60, halfB_out_ga(T26, s(s(T34)))) → U45_ga(T12, T60, halfB_in_ga(T34, s(s(T42))))
U45_ga(T12, T60, halfB_out_ga(T34, s(s(T42)))) → U46_ga(T12, T60, halfB_in_ga(T42, s(s(T50))))
U46_ga(T12, T60, halfB_out_ga(T42, s(s(T50)))) → U47_ga(T12, T60, halfB_in_ga(T50, s(s(T58))))
U47_ga(T12, T60, halfB_out_ga(T50, s(s(T58)))) → U48_ga(T12, T60, halfB_in_ga(T58, X159))
U48_ga(T12, T60, halfB_out_ga(T58, X159)) → log2D_out_ga(s(s(T12)), T60)
log2D_in_ga(s(s(T12)), s(s(s(s(s(s(0))))))) → U49_ga(T12, halfB_in_ga(T12, s(s(T26))))
U49_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U50_ga(T12, halfB_in_ga(T26, s(s(T34))))
U50_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U51_ga(T12, halfB_in_ga(T34, s(s(T42))))
U51_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U52_ga(T12, halfB_in_ga(T42, s(s(T50))))
U52_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U53_ga(T12, halfB_in_ga(T50, s(s(T58))))
U53_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U54_ga(T12, halfB_in_gg(T58, 0))
U54_ga(T12, halfB_out_gg(T58, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
U53_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U55_ga(T12, halfB_in_gg(T58, s(0)))
U55_ga(T12, halfB_out_gg(T58, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
log2D_in_ga(s(s(T12)), T68) → U56_ga(T12, T68, halfB_in_ga(T12, s(s(T26))))
U56_ga(T12, T68, halfB_out_ga(T12, s(s(T26)))) → U57_ga(T12, T68, halfB_in_ga(T26, s(s(T34))))
U57_ga(T12, T68, halfB_out_ga(T26, s(s(T34)))) → U58_ga(T12, T68, halfB_in_ga(T34, s(s(T42))))
U58_ga(T12, T68, halfB_out_ga(T34, s(s(T42)))) → U59_ga(T12, T68, halfB_in_ga(T42, s(s(T50))))
U59_ga(T12, T68, halfB_out_ga(T42, s(s(T50)))) → U60_ga(T12, T68, halfB_in_ga(T50, s(s(T58))))
U60_ga(T12, T68, halfB_out_ga(T50, s(s(T58)))) → U61_ga(T12, T68, halfB_in_ga(T58, s(s(T66))))
U61_ga(T12, T68, halfB_out_ga(T58, s(s(T66)))) → U62_ga(T12, T68, halfB_in_ga(T66, X182))
U62_ga(T12, T68, halfB_out_ga(T66, X182)) → log2D_out_ga(s(s(T12)), T68)
log2D_in_ga(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → U63_ga(T12, halfB_in_ga(T12, s(s(T26))))
U63_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U64_ga(T12, halfB_in_ga(T26, s(s(T34))))
U64_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U65_ga(T12, halfB_in_ga(T34, s(s(T42))))
U65_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U66_ga(T12, halfB_in_ga(T42, s(s(T50))))
U66_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U67_ga(T12, halfB_in_ga(T50, s(s(T58))))
U67_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U68_ga(T12, halfB_in_ga(T58, s(s(T66))))
U68_ga(T12, halfB_out_ga(T58, s(s(T66)))) → U69_ga(T12, halfB_in_gg(T66, 0))
U69_ga(T12, halfB_out_gg(T66, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
U68_ga(T12, halfB_out_ga(T58, s(s(T66)))) → U70_ga(T12, halfB_in_gg(T66, s(0)))
U70_ga(T12, halfB_out_gg(T66, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
log2D_in_ga(s(s(T12)), T76) → U71_ga(T12, T76, halfB_in_ga(T12, s(s(T26))))
U71_ga(T12, T76, halfB_out_ga(T12, s(s(T26)))) → U72_ga(T12, T76, halfB_in_ga(T26, s(s(T34))))
U72_ga(T12, T76, halfB_out_ga(T26, s(s(T34)))) → U73_ga(T12, T76, halfB_in_ga(T34, s(s(T42))))
U73_ga(T12, T76, halfB_out_ga(T34, s(s(T42)))) → U74_ga(T12, T76, halfB_in_ga(T42, s(s(T50))))
U74_ga(T12, T76, halfB_out_ga(T42, s(s(T50)))) → U75_ga(T12, T76, halfB_in_ga(T50, s(s(T58))))
U75_ga(T12, T76, halfB_out_ga(T50, s(s(T58)))) → U76_ga(T12, T76, halfB_in_ga(T58, s(s(T66))))
U76_ga(T12, T76, halfB_out_ga(T58, s(s(T66)))) → U77_ga(T12, T76, halfB_in_ga(T66, s(s(T74))))
U77_ga(T12, T76, halfB_out_ga(T66, s(s(T74)))) → U78_ga(T12, T76, pC_in_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76))
pC_in_gaga(T74, X205, T77, T76) → U3_gaga(T74, X205, T77, T76, halfB_in_ga(T74, X205))
U3_gaga(T74, X205, T77, T76, halfB_out_ga(T74, X205)) → pC_out_gaga(T74, X205, T77, T76)
pC_in_gaga(T74, 0, T85, s(T85)) → U4_gaga(T74, T85, halfB_in_gg(T74, 0))
U4_gaga(T74, T85, halfB_out_gg(T74, 0)) → pC_out_gaga(T74, 0, T85, s(T85))
pC_in_gaga(T74, s(0), T90, s(T90)) → U5_gaga(T74, T90, halfB_in_gg(T74, s(0)))
U5_gaga(T74, T90, halfB_out_gg(T74, s(0))) → pC_out_gaga(T74, s(0), T90, s(T90))
pC_in_gaga(T74, s(s(T97)), T98, T100) → U6_gaga(T74, T97, T98, T100, halfB_in_ga(T74, s(s(T97))))
U6_gaga(T74, T97, T98, T100, halfB_out_ga(T74, s(s(T97)))) → U7_gaga(T74, T97, T98, T100, pC_in_gaga(T97, X228, s(T98), T100))
U7_gaga(T74, T97, T98, T100, pC_out_gaga(T97, X228, s(T98), T100)) → pC_out_gaga(T74, s(s(T97)), T98, T100)
U78_ga(T12, T76, pC_out_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76)) → log2D_out_ga(s(s(T12)), T76)

The argument filtering Pi contains the following mapping:
log2D_in_ga(x1, x2)  =  log2D_in_ga(x1)
0  =  0
log2D_out_ga(x1, x2)  =  log2D_out_ga
s(x1)  =  s(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
halfB_in_ga(x1, x2)  =  halfB_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
halfA_in_ga(x1, x2)  =  halfA_in_ga(x1)
halfA_out_ga(x1, x2)  =  halfA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
halfB_out_ga(x1, x2)  =  halfB_out_ga(x2)
U9_ga(x1, x2)  =  U9_ga(x2)
halfB_in_gg(x1, x2)  =  halfB_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
halfA_in_gg(x1, x2)  =  halfA_in_gg(x1, x2)
halfA_out_gg(x1, x2)  =  halfA_out_gg
U1_gg(x1, x2, x3)  =  U1_gg(x3)
halfB_out_gg(x1, x2)  =  halfB_out_gg
U10_ga(x1, x2)  =  U10_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2)  =  U13_ga(x2)
U14_ga(x1, x2)  =  U14_ga(x2)
U15_ga(x1, x2)  =  U15_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
U18_ga(x1, x2, x3)  =  U18_ga(x3)
U19_ga(x1, x2)  =  U19_ga(x2)
U20_ga(x1, x2)  =  U20_ga(x2)
U21_ga(x1, x2)  =  U21_ga(x2)
U22_ga(x1, x2)  =  U22_ga(x2)
U23_ga(x1, x2, x3)  =  U23_ga(x3)
U24_ga(x1, x2, x3)  =  U24_ga(x3)
U25_ga(x1, x2, x3)  =  U25_ga(x3)
U26_ga(x1, x2, x3)  =  U26_ga(x3)
U27_ga(x1, x2)  =  U27_ga(x2)
U28_ga(x1, x2)  =  U28_ga(x2)
U29_ga(x1, x2)  =  U29_ga(x2)
U30_ga(x1, x2)  =  U30_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U33_ga(x1, x2, x3)  =  U33_ga(x3)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
U35_ga(x1, x2, x3)  =  U35_ga(x3)
U36_ga(x1, x2, x3)  =  U36_ga(x3)
U37_ga(x1, x2)  =  U37_ga(x2)
U38_ga(x1, x2)  =  U38_ga(x2)
U39_ga(x1, x2)  =  U39_ga(x2)
U40_ga(x1, x2)  =  U40_ga(x2)
U41_ga(x1, x2)  =  U41_ga(x2)
U42_ga(x1, x2)  =  U42_ga(x2)
U43_ga(x1, x2, x3)  =  U43_ga(x3)
U44_ga(x1, x2, x3)  =  U44_ga(x3)
U45_ga(x1, x2, x3)  =  U45_ga(x3)
U46_ga(x1, x2, x3)  =  U46_ga(x3)
U47_ga(x1, x2, x3)  =  U47_ga(x3)
U48_ga(x1, x2, x3)  =  U48_ga(x3)
U49_ga(x1, x2)  =  U49_ga(x2)
U50_ga(x1, x2)  =  U50_ga(x2)
U51_ga(x1, x2)  =  U51_ga(x2)
U52_ga(x1, x2)  =  U52_ga(x2)
U53_ga(x1, x2)  =  U53_ga(x2)
U54_ga(x1, x2)  =  U54_ga(x2)
U55_ga(x1, x2)  =  U55_ga(x2)
U56_ga(x1, x2, x3)  =  U56_ga(x3)
U57_ga(x1, x2, x3)  =  U57_ga(x3)
U58_ga(x1, x2, x3)  =  U58_ga(x3)
U59_ga(x1, x2, x3)  =  U59_ga(x3)
U60_ga(x1, x2, x3)  =  U60_ga(x3)
U61_ga(x1, x2, x3)  =  U61_ga(x3)
U62_ga(x1, x2, x3)  =  U62_ga(x3)
U63_ga(x1, x2)  =  U63_ga(x2)
U64_ga(x1, x2)  =  U64_ga(x2)
U65_ga(x1, x2)  =  U65_ga(x2)
U66_ga(x1, x2)  =  U66_ga(x2)
U67_ga(x1, x2)  =  U67_ga(x2)
U68_ga(x1, x2)  =  U68_ga(x2)
U69_ga(x1, x2)  =  U69_ga(x2)
U70_ga(x1, x2)  =  U70_ga(x2)
U71_ga(x1, x2, x3)  =  U71_ga(x3)
U72_ga(x1, x2, x3)  =  U72_ga(x3)
U73_ga(x1, x2, x3)  =  U73_ga(x3)
U74_ga(x1, x2, x3)  =  U74_ga(x3)
U75_ga(x1, x2, x3)  =  U75_ga(x3)
U76_ga(x1, x2, x3)  =  U76_ga(x3)
U77_ga(x1, x2, x3)  =  U77_ga(x3)
U78_ga(x1, x2, x3)  =  U78_ga(x3)
pC_in_gaga(x1, x2, x3, x4)  =  pC_in_gaga(x1, x3)
U3_gaga(x1, x2, x3, x4, x5)  =  U3_gaga(x5)
pC_out_gaga(x1, x2, x3, x4)  =  pC_out_gaga(x2)
U4_gaga(x1, x2, x3)  =  U4_gaga(x3)
U5_gaga(x1, x2, x3)  =  U5_gaga(x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x3, x5)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x2, x5)
LOG2D_IN_GA(x1, x2)  =  LOG2D_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x3)
HALFB_IN_GA(x1, x2)  =  HALFB_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
HALFA_IN_GA(x1, x2)  =  HALFA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U9_GA(x1, x2)  =  U9_GA(x2)
HALFB_IN_GG(x1, x2)  =  HALFB_IN_GG(x1, x2)
U2_GG(x1, x2, x3)  =  U2_GG(x3)
HALFA_IN_GG(x1, x2)  =  HALFA_IN_GG(x1, x2)
U1_GG(x1, x2, x3)  =  U1_GG(x3)
U10_GA(x1, x2)  =  U10_GA(x2)
U11_GA(x1, x2, x3)  =  U11_GA(x3)
U12_GA(x1, x2, x3)  =  U12_GA(x3)
U13_GA(x1, x2)  =  U13_GA(x2)
U14_GA(x1, x2)  =  U14_GA(x2)
U15_GA(x1, x2)  =  U15_GA(x2)
U16_GA(x1, x2, x3)  =  U16_GA(x3)
U17_GA(x1, x2, x3)  =  U17_GA(x3)
U18_GA(x1, x2, x3)  =  U18_GA(x3)
U19_GA(x1, x2)  =  U19_GA(x2)
U20_GA(x1, x2)  =  U20_GA(x2)
U21_GA(x1, x2)  =  U21_GA(x2)
U22_GA(x1, x2)  =  U22_GA(x2)
U23_GA(x1, x2, x3)  =  U23_GA(x3)
U24_GA(x1, x2, x3)  =  U24_GA(x3)
U25_GA(x1, x2, x3)  =  U25_GA(x3)
U26_GA(x1, x2, x3)  =  U26_GA(x3)
U27_GA(x1, x2)  =  U27_GA(x2)
U28_GA(x1, x2)  =  U28_GA(x2)
U29_GA(x1, x2)  =  U29_GA(x2)
U30_GA(x1, x2)  =  U30_GA(x2)
U31_GA(x1, x2)  =  U31_GA(x2)
U32_GA(x1, x2, x3)  =  U32_GA(x3)
U33_GA(x1, x2, x3)  =  U33_GA(x3)
U34_GA(x1, x2, x3)  =  U34_GA(x3)
U35_GA(x1, x2, x3)  =  U35_GA(x3)
U36_GA(x1, x2, x3)  =  U36_GA(x3)
U37_GA(x1, x2)  =  U37_GA(x2)
U38_GA(x1, x2)  =  U38_GA(x2)
U39_GA(x1, x2)  =  U39_GA(x2)
U40_GA(x1, x2)  =  U40_GA(x2)
U41_GA(x1, x2)  =  U41_GA(x2)
U42_GA(x1, x2)  =  U42_GA(x2)
U43_GA(x1, x2, x3)  =  U43_GA(x3)
U44_GA(x1, x2, x3)  =  U44_GA(x3)
U45_GA(x1, x2, x3)  =  U45_GA(x3)
U46_GA(x1, x2, x3)  =  U46_GA(x3)
U47_GA(x1, x2, x3)  =  U47_GA(x3)
U48_GA(x1, x2, x3)  =  U48_GA(x3)
U49_GA(x1, x2)  =  U49_GA(x2)
U50_GA(x1, x2)  =  U50_GA(x2)
U51_GA(x1, x2)  =  U51_GA(x2)
U52_GA(x1, x2)  =  U52_GA(x2)
U53_GA(x1, x2)  =  U53_GA(x2)
U54_GA(x1, x2)  =  U54_GA(x2)
U55_GA(x1, x2)  =  U55_GA(x2)
U56_GA(x1, x2, x3)  =  U56_GA(x3)
U57_GA(x1, x2, x3)  =  U57_GA(x3)
U58_GA(x1, x2, x3)  =  U58_GA(x3)
U59_GA(x1, x2, x3)  =  U59_GA(x3)
U60_GA(x1, x2, x3)  =  U60_GA(x3)
U61_GA(x1, x2, x3)  =  U61_GA(x3)
U62_GA(x1, x2, x3)  =  U62_GA(x3)
U63_GA(x1, x2)  =  U63_GA(x2)
U64_GA(x1, x2)  =  U64_GA(x2)
U65_GA(x1, x2)  =  U65_GA(x2)
U66_GA(x1, x2)  =  U66_GA(x2)
U67_GA(x1, x2)  =  U67_GA(x2)
U68_GA(x1, x2)  =  U68_GA(x2)
U69_GA(x1, x2)  =  U69_GA(x2)
U70_GA(x1, x2)  =  U70_GA(x2)
U71_GA(x1, x2, x3)  =  U71_GA(x3)
U72_GA(x1, x2, x3)  =  U72_GA(x3)
U73_GA(x1, x2, x3)  =  U73_GA(x3)
U74_GA(x1, x2, x3)  =  U74_GA(x3)
U75_GA(x1, x2, x3)  =  U75_GA(x3)
U76_GA(x1, x2, x3)  =  U76_GA(x3)
U77_GA(x1, x2, x3)  =  U77_GA(x3)
U78_GA(x1, x2, x3)  =  U78_GA(x3)
PC_IN_GAGA(x1, x2, x3, x4)  =  PC_IN_GAGA(x1, x3)
U3_GAGA(x1, x2, x3, x4, x5)  =  U3_GAGA(x5)
U4_GAGA(x1, x2, x3)  =  U4_GAGA(x3)
U5_GAGA(x1, x2, x3)  =  U5_GAGA(x3)
U6_GAGA(x1, x2, x3, x4, x5)  =  U6_GAGA(x3, x5)
U7_GAGA(x1, x2, x3, x4, x5)  =  U7_GAGA(x2, x5)

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LOG2D_IN_GA(s(s(T12)), T14) → U8_GA(T12, T14, halfB_in_ga(T12, X26))
LOG2D_IN_GA(s(s(T12)), T14) → HALFB_IN_GA(T12, X26)
HALFB_IN_GA(T18, s(X35)) → U2_GA(T18, X35, halfA_in_ga(T18, X35))
HALFB_IN_GA(T18, s(X35)) → HALFA_IN_GA(T18, X35)
HALFA_IN_GA(s(s(T21)), s(X44)) → U1_GA(T21, X44, halfA_in_ga(T21, X44))
HALFA_IN_GA(s(s(T21)), s(X44)) → HALFA_IN_GA(T21, X44)
LOG2D_IN_GA(s(s(T12)), s(0)) → U9_GA(T12, halfB_in_gg(T12, 0))
LOG2D_IN_GA(s(s(T12)), s(0)) → HALFB_IN_GG(T12, 0)
HALFB_IN_GG(T18, s(X35)) → U2_GG(T18, X35, halfA_in_gg(T18, X35))
HALFB_IN_GG(T18, s(X35)) → HALFA_IN_GG(T18, X35)
HALFA_IN_GG(s(s(T21)), s(X44)) → U1_GG(T21, X44, halfA_in_gg(T21, X44))
HALFA_IN_GG(s(s(T21)), s(X44)) → HALFA_IN_GG(T21, X44)
LOG2D_IN_GA(s(s(T12)), s(0)) → U10_GA(T12, halfB_in_gg(T12, s(0)))
LOG2D_IN_GA(s(s(T12)), s(0)) → HALFB_IN_GG(T12, s(0))
LOG2D_IN_GA(s(s(T12)), T28) → U11_GA(T12, T28, halfB_in_ga(T12, s(s(T26))))
LOG2D_IN_GA(s(s(T12)), T28) → HALFB_IN_GA(T12, s(s(T26)))
U11_GA(T12, T28, halfB_out_ga(T12, s(s(T26)))) → U12_GA(T12, T28, halfB_in_ga(T26, X67))
U11_GA(T12, T28, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, X67)
LOG2D_IN_GA(s(s(T12)), s(s(0))) → U13_GA(T12, halfB_in_ga(T12, s(s(T26))))
LOG2D_IN_GA(s(s(T12)), s(s(0))) → HALFB_IN_GA(T12, s(s(T26)))
U13_GA(T12, halfB_out_ga(T12, s(s(T26)))) → U14_GA(T12, halfB_in_gg(T26, 0))
U13_GA(T12, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GG(T26, 0)
U13_GA(T12, halfB_out_ga(T12, s(s(T26)))) → U15_GA(T12, halfB_in_gg(T26, s(0)))
U13_GA(T12, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GG(T26, s(0))
LOG2D_IN_GA(s(s(T12)), T36) → U16_GA(T12, T36, halfB_in_ga(T12, s(s(T26))))
U16_GA(T12, T36, halfB_out_ga(T12, s(s(T26)))) → U17_GA(T12, T36, halfB_in_ga(T26, s(s(T34))))
U16_GA(T12, T36, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U17_GA(T12, T36, halfB_out_ga(T26, s(s(T34)))) → U18_GA(T12, T36, halfB_in_ga(T34, X90))
U17_GA(T12, T36, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, X90)
LOG2D_IN_GA(s(s(T12)), s(s(s(0)))) → U19_GA(T12, halfB_in_ga(T12, s(s(T26))))
LOG2D_IN_GA(s(s(T12)), s(s(s(0)))) → HALFB_IN_GA(T12, s(s(T26)))
U19_GA(T12, halfB_out_ga(T12, s(s(T26)))) → U20_GA(T12, halfB_in_ga(T26, s(s(T34))))
U19_GA(T12, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U20_GA(T12, halfB_out_ga(T26, s(s(T34)))) → U21_GA(T12, halfB_in_gg(T34, 0))
U20_GA(T12, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GG(T34, 0)
U20_GA(T12, halfB_out_ga(T26, s(s(T34)))) → U22_GA(T12, halfB_in_gg(T34, s(0)))
U20_GA(T12, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GG(T34, s(0))
LOG2D_IN_GA(s(s(T12)), T44) → U23_GA(T12, T44, halfB_in_ga(T12, s(s(T26))))
U23_GA(T12, T44, halfB_out_ga(T12, s(s(T26)))) → U24_GA(T12, T44, halfB_in_ga(T26, s(s(T34))))
U23_GA(T12, T44, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U24_GA(T12, T44, halfB_out_ga(T26, s(s(T34)))) → U25_GA(T12, T44, halfB_in_ga(T34, s(s(T42))))
U24_GA(T12, T44, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, s(s(T42)))
U25_GA(T12, T44, halfB_out_ga(T34, s(s(T42)))) → U26_GA(T12, T44, halfB_in_ga(T42, X113))
U25_GA(T12, T44, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GA(T42, X113)
LOG2D_IN_GA(s(s(T12)), s(s(s(s(0))))) → U27_GA(T12, halfB_in_ga(T12, s(s(T26))))
LOG2D_IN_GA(s(s(T12)), s(s(s(s(0))))) → HALFB_IN_GA(T12, s(s(T26)))
U27_GA(T12, halfB_out_ga(T12, s(s(T26)))) → U28_GA(T12, halfB_in_ga(T26, s(s(T34))))
U27_GA(T12, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U28_GA(T12, halfB_out_ga(T26, s(s(T34)))) → U29_GA(T12, halfB_in_ga(T34, s(s(T42))))
U28_GA(T12, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, s(s(T42)))
U29_GA(T12, halfB_out_ga(T34, s(s(T42)))) → U30_GA(T12, halfB_in_gg(T42, 0))
U29_GA(T12, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GG(T42, 0)
U29_GA(T12, halfB_out_ga(T34, s(s(T42)))) → U31_GA(T12, halfB_in_gg(T42, s(0)))
U29_GA(T12, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GG(T42, s(0))
LOG2D_IN_GA(s(s(T12)), T52) → U32_GA(T12, T52, halfB_in_ga(T12, s(s(T26))))
U32_GA(T12, T52, halfB_out_ga(T12, s(s(T26)))) → U33_GA(T12, T52, halfB_in_ga(T26, s(s(T34))))
U32_GA(T12, T52, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U33_GA(T12, T52, halfB_out_ga(T26, s(s(T34)))) → U34_GA(T12, T52, halfB_in_ga(T34, s(s(T42))))
U33_GA(T12, T52, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, s(s(T42)))
U34_GA(T12, T52, halfB_out_ga(T34, s(s(T42)))) → U35_GA(T12, T52, halfB_in_ga(T42, s(s(T50))))
U34_GA(T12, T52, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GA(T42, s(s(T50)))
U35_GA(T12, T52, halfB_out_ga(T42, s(s(T50)))) → U36_GA(T12, T52, halfB_in_ga(T50, X136))
U35_GA(T12, T52, halfB_out_ga(T42, s(s(T50)))) → HALFB_IN_GA(T50, X136)
LOG2D_IN_GA(s(s(T12)), s(s(s(s(s(0)))))) → U37_GA(T12, halfB_in_ga(T12, s(s(T26))))
LOG2D_IN_GA(s(s(T12)), s(s(s(s(s(0)))))) → HALFB_IN_GA(T12, s(s(T26)))
U37_GA(T12, halfB_out_ga(T12, s(s(T26)))) → U38_GA(T12, halfB_in_ga(T26, s(s(T34))))
U37_GA(T12, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U38_GA(T12, halfB_out_ga(T26, s(s(T34)))) → U39_GA(T12, halfB_in_ga(T34, s(s(T42))))
U38_GA(T12, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, s(s(T42)))
U39_GA(T12, halfB_out_ga(T34, s(s(T42)))) → U40_GA(T12, halfB_in_ga(T42, s(s(T50))))
U39_GA(T12, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GA(T42, s(s(T50)))
U40_GA(T12, halfB_out_ga(T42, s(s(T50)))) → U41_GA(T12, halfB_in_gg(T50, 0))
U40_GA(T12, halfB_out_ga(T42, s(s(T50)))) → HALFB_IN_GG(T50, 0)
U40_GA(T12, halfB_out_ga(T42, s(s(T50)))) → U42_GA(T12, halfB_in_gg(T50, s(0)))
U40_GA(T12, halfB_out_ga(T42, s(s(T50)))) → HALFB_IN_GG(T50, s(0))
LOG2D_IN_GA(s(s(T12)), T60) → U43_GA(T12, T60, halfB_in_ga(T12, s(s(T26))))
U43_GA(T12, T60, halfB_out_ga(T12, s(s(T26)))) → U44_GA(T12, T60, halfB_in_ga(T26, s(s(T34))))
U43_GA(T12, T60, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U44_GA(T12, T60, halfB_out_ga(T26, s(s(T34)))) → U45_GA(T12, T60, halfB_in_ga(T34, s(s(T42))))
U44_GA(T12, T60, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, s(s(T42)))
U45_GA(T12, T60, halfB_out_ga(T34, s(s(T42)))) → U46_GA(T12, T60, halfB_in_ga(T42, s(s(T50))))
U45_GA(T12, T60, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GA(T42, s(s(T50)))
U46_GA(T12, T60, halfB_out_ga(T42, s(s(T50)))) → U47_GA(T12, T60, halfB_in_ga(T50, s(s(T58))))
U46_GA(T12, T60, halfB_out_ga(T42, s(s(T50)))) → HALFB_IN_GA(T50, s(s(T58)))
U47_GA(T12, T60, halfB_out_ga(T50, s(s(T58)))) → U48_GA(T12, T60, halfB_in_ga(T58, X159))
U47_GA(T12, T60, halfB_out_ga(T50, s(s(T58)))) → HALFB_IN_GA(T58, X159)
LOG2D_IN_GA(s(s(T12)), s(s(s(s(s(s(0))))))) → U49_GA(T12, halfB_in_ga(T12, s(s(T26))))
LOG2D_IN_GA(s(s(T12)), s(s(s(s(s(s(0))))))) → HALFB_IN_GA(T12, s(s(T26)))
U49_GA(T12, halfB_out_ga(T12, s(s(T26)))) → U50_GA(T12, halfB_in_ga(T26, s(s(T34))))
U49_GA(T12, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U50_GA(T12, halfB_out_ga(T26, s(s(T34)))) → U51_GA(T12, halfB_in_ga(T34, s(s(T42))))
U50_GA(T12, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, s(s(T42)))
U51_GA(T12, halfB_out_ga(T34, s(s(T42)))) → U52_GA(T12, halfB_in_ga(T42, s(s(T50))))
U51_GA(T12, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GA(T42, s(s(T50)))
U52_GA(T12, halfB_out_ga(T42, s(s(T50)))) → U53_GA(T12, halfB_in_ga(T50, s(s(T58))))
U52_GA(T12, halfB_out_ga(T42, s(s(T50)))) → HALFB_IN_GA(T50, s(s(T58)))
U53_GA(T12, halfB_out_ga(T50, s(s(T58)))) → U54_GA(T12, halfB_in_gg(T58, 0))
U53_GA(T12, halfB_out_ga(T50, s(s(T58)))) → HALFB_IN_GG(T58, 0)
U53_GA(T12, halfB_out_ga(T50, s(s(T58)))) → U55_GA(T12, halfB_in_gg(T58, s(0)))
U53_GA(T12, halfB_out_ga(T50, s(s(T58)))) → HALFB_IN_GG(T58, s(0))
LOG2D_IN_GA(s(s(T12)), T68) → U56_GA(T12, T68, halfB_in_ga(T12, s(s(T26))))
U56_GA(T12, T68, halfB_out_ga(T12, s(s(T26)))) → U57_GA(T12, T68, halfB_in_ga(T26, s(s(T34))))
U56_GA(T12, T68, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U57_GA(T12, T68, halfB_out_ga(T26, s(s(T34)))) → U58_GA(T12, T68, halfB_in_ga(T34, s(s(T42))))
U57_GA(T12, T68, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, s(s(T42)))
U58_GA(T12, T68, halfB_out_ga(T34, s(s(T42)))) → U59_GA(T12, T68, halfB_in_ga(T42, s(s(T50))))
U58_GA(T12, T68, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GA(T42, s(s(T50)))
U59_GA(T12, T68, halfB_out_ga(T42, s(s(T50)))) → U60_GA(T12, T68, halfB_in_ga(T50, s(s(T58))))
U59_GA(T12, T68, halfB_out_ga(T42, s(s(T50)))) → HALFB_IN_GA(T50, s(s(T58)))
U60_GA(T12, T68, halfB_out_ga(T50, s(s(T58)))) → U61_GA(T12, T68, halfB_in_ga(T58, s(s(T66))))
U60_GA(T12, T68, halfB_out_ga(T50, s(s(T58)))) → HALFB_IN_GA(T58, s(s(T66)))
U61_GA(T12, T68, halfB_out_ga(T58, s(s(T66)))) → U62_GA(T12, T68, halfB_in_ga(T66, X182))
U61_GA(T12, T68, halfB_out_ga(T58, s(s(T66)))) → HALFB_IN_GA(T66, X182)
LOG2D_IN_GA(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → U63_GA(T12, halfB_in_ga(T12, s(s(T26))))
LOG2D_IN_GA(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → HALFB_IN_GA(T12, s(s(T26)))
U63_GA(T12, halfB_out_ga(T12, s(s(T26)))) → U64_GA(T12, halfB_in_ga(T26, s(s(T34))))
U63_GA(T12, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U64_GA(T12, halfB_out_ga(T26, s(s(T34)))) → U65_GA(T12, halfB_in_ga(T34, s(s(T42))))
U64_GA(T12, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, s(s(T42)))
U65_GA(T12, halfB_out_ga(T34, s(s(T42)))) → U66_GA(T12, halfB_in_ga(T42, s(s(T50))))
U65_GA(T12, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GA(T42, s(s(T50)))
U66_GA(T12, halfB_out_ga(T42, s(s(T50)))) → U67_GA(T12, halfB_in_ga(T50, s(s(T58))))
U66_GA(T12, halfB_out_ga(T42, s(s(T50)))) → HALFB_IN_GA(T50, s(s(T58)))
U67_GA(T12, halfB_out_ga(T50, s(s(T58)))) → U68_GA(T12, halfB_in_ga(T58, s(s(T66))))
U67_GA(T12, halfB_out_ga(T50, s(s(T58)))) → HALFB_IN_GA(T58, s(s(T66)))
U68_GA(T12, halfB_out_ga(T58, s(s(T66)))) → U69_GA(T12, halfB_in_gg(T66, 0))
U68_GA(T12, halfB_out_ga(T58, s(s(T66)))) → HALFB_IN_GG(T66, 0)
U68_GA(T12, halfB_out_ga(T58, s(s(T66)))) → U70_GA(T12, halfB_in_gg(T66, s(0)))
U68_GA(T12, halfB_out_ga(T58, s(s(T66)))) → HALFB_IN_GG(T66, s(0))
LOG2D_IN_GA(s(s(T12)), T76) → U71_GA(T12, T76, halfB_in_ga(T12, s(s(T26))))
U71_GA(T12, T76, halfB_out_ga(T12, s(s(T26)))) → U72_GA(T12, T76, halfB_in_ga(T26, s(s(T34))))
U71_GA(T12, T76, halfB_out_ga(T12, s(s(T26)))) → HALFB_IN_GA(T26, s(s(T34)))
U72_GA(T12, T76, halfB_out_ga(T26, s(s(T34)))) → U73_GA(T12, T76, halfB_in_ga(T34, s(s(T42))))
U72_GA(T12, T76, halfB_out_ga(T26, s(s(T34)))) → HALFB_IN_GA(T34, s(s(T42)))
U73_GA(T12, T76, halfB_out_ga(T34, s(s(T42)))) → U74_GA(T12, T76, halfB_in_ga(T42, s(s(T50))))
U73_GA(T12, T76, halfB_out_ga(T34, s(s(T42)))) → HALFB_IN_GA(T42, s(s(T50)))
U74_GA(T12, T76, halfB_out_ga(T42, s(s(T50)))) → U75_GA(T12, T76, halfB_in_ga(T50, s(s(T58))))
U74_GA(T12, T76, halfB_out_ga(T42, s(s(T50)))) → HALFB_IN_GA(T50, s(s(T58)))
U75_GA(T12, T76, halfB_out_ga(T50, s(s(T58)))) → U76_GA(T12, T76, halfB_in_ga(T58, s(s(T66))))
U75_GA(T12, T76, halfB_out_ga(T50, s(s(T58)))) → HALFB_IN_GA(T58, s(s(T66)))
U76_GA(T12, T76, halfB_out_ga(T58, s(s(T66)))) → U77_GA(T12, T76, halfB_in_ga(T66, s(s(T74))))
U76_GA(T12, T76, halfB_out_ga(T58, s(s(T66)))) → HALFB_IN_GA(T66, s(s(T74)))
U77_GA(T12, T76, halfB_out_ga(T66, s(s(T74)))) → U78_GA(T12, T76, pC_in_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76))
U77_GA(T12, T76, halfB_out_ga(T66, s(s(T74)))) → PC_IN_GAGA(T74, X205, s(s(s(s(s(s(s(0))))))), T76)
PC_IN_GAGA(T74, X205, T77, T76) → U3_GAGA(T74, X205, T77, T76, halfB_in_ga(T74, X205))
PC_IN_GAGA(T74, X205, T77, T76) → HALFB_IN_GA(T74, X205)
PC_IN_GAGA(T74, 0, T85, s(T85)) → U4_GAGA(T74, T85, halfB_in_gg(T74, 0))
PC_IN_GAGA(T74, 0, T85, s(T85)) → HALFB_IN_GG(T74, 0)
PC_IN_GAGA(T74, s(0), T90, s(T90)) → U5_GAGA(T74, T90, halfB_in_gg(T74, s(0)))
PC_IN_GAGA(T74, s(0), T90, s(T90)) → HALFB_IN_GG(T74, s(0))
PC_IN_GAGA(T74, s(s(T97)), T98, T100) → U6_GAGA(T74, T97, T98, T100, halfB_in_ga(T74, s(s(T97))))
PC_IN_GAGA(T74, s(s(T97)), T98, T100) → HALFB_IN_GA(T74, s(s(T97)))
U6_GAGA(T74, T97, T98, T100, halfB_out_ga(T74, s(s(T97)))) → U7_GAGA(T74, T97, T98, T100, pC_in_gaga(T97, X228, s(T98), T100))
U6_GAGA(T74, T97, T98, T100, halfB_out_ga(T74, s(s(T97)))) → PC_IN_GAGA(T97, X228, s(T98), T100)

The TRS R consists of the following rules:

log2D_in_ga(0, 0) → log2D_out_ga(0, 0)
log2D_in_ga(s(0), 0) → log2D_out_ga(s(0), 0)
log2D_in_ga(s(s(T12)), T14) → U8_ga(T12, T14, halfB_in_ga(T12, X26))
halfB_in_ga(T18, s(X35)) → U2_ga(T18, X35, halfA_in_ga(T18, X35))
halfA_in_ga(0, 0) → halfA_out_ga(0, 0)
halfA_in_ga(s(0), 0) → halfA_out_ga(s(0), 0)
halfA_in_ga(s(s(T21)), s(X44)) → U1_ga(T21, X44, halfA_in_ga(T21, X44))
U1_ga(T21, X44, halfA_out_ga(T21, X44)) → halfA_out_ga(s(s(T21)), s(X44))
U2_ga(T18, X35, halfA_out_ga(T18, X35)) → halfB_out_ga(T18, s(X35))
U8_ga(T12, T14, halfB_out_ga(T12, X26)) → log2D_out_ga(s(s(T12)), T14)
log2D_in_ga(s(s(T12)), s(0)) → U9_ga(T12, halfB_in_gg(T12, 0))
halfB_in_gg(T18, s(X35)) → U2_gg(T18, X35, halfA_in_gg(T18, X35))
halfA_in_gg(0, 0) → halfA_out_gg(0, 0)
halfA_in_gg(s(0), 0) → halfA_out_gg(s(0), 0)
halfA_in_gg(s(s(T21)), s(X44)) → U1_gg(T21, X44, halfA_in_gg(T21, X44))
U1_gg(T21, X44, halfA_out_gg(T21, X44)) → halfA_out_gg(s(s(T21)), s(X44))
U2_gg(T18, X35, halfA_out_gg(T18, X35)) → halfB_out_gg(T18, s(X35))
U9_ga(T12, halfB_out_gg(T12, 0)) → log2D_out_ga(s(s(T12)), s(0))
log2D_in_ga(s(s(T12)), s(0)) → U10_ga(T12, halfB_in_gg(T12, s(0)))
U10_ga(T12, halfB_out_gg(T12, s(0))) → log2D_out_ga(s(s(T12)), s(0))
log2D_in_ga(s(s(T12)), T28) → U11_ga(T12, T28, halfB_in_ga(T12, s(s(T26))))
U11_ga(T12, T28, halfB_out_ga(T12, s(s(T26)))) → U12_ga(T12, T28, halfB_in_ga(T26, X67))
U12_ga(T12, T28, halfB_out_ga(T26, X67)) → log2D_out_ga(s(s(T12)), T28)
log2D_in_ga(s(s(T12)), s(s(0))) → U13_ga(T12, halfB_in_ga(T12, s(s(T26))))
U13_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U14_ga(T12, halfB_in_gg(T26, 0))
U14_ga(T12, halfB_out_gg(T26, 0)) → log2D_out_ga(s(s(T12)), s(s(0)))
U13_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U15_ga(T12, halfB_in_gg(T26, s(0)))
U15_ga(T12, halfB_out_gg(T26, s(0))) → log2D_out_ga(s(s(T12)), s(s(0)))
log2D_in_ga(s(s(T12)), T36) → U16_ga(T12, T36, halfB_in_ga(T12, s(s(T26))))
U16_ga(T12, T36, halfB_out_ga(T12, s(s(T26)))) → U17_ga(T12, T36, halfB_in_ga(T26, s(s(T34))))
U17_ga(T12, T36, halfB_out_ga(T26, s(s(T34)))) → U18_ga(T12, T36, halfB_in_ga(T34, X90))
U18_ga(T12, T36, halfB_out_ga(T34, X90)) → log2D_out_ga(s(s(T12)), T36)
log2D_in_ga(s(s(T12)), s(s(s(0)))) → U19_ga(T12, halfB_in_ga(T12, s(s(T26))))
U19_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U20_ga(T12, halfB_in_ga(T26, s(s(T34))))
U20_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U21_ga(T12, halfB_in_gg(T34, 0))
U21_ga(T12, halfB_out_gg(T34, 0)) → log2D_out_ga(s(s(T12)), s(s(s(0))))
U20_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U22_ga(T12, halfB_in_gg(T34, s(0)))
U22_ga(T12, halfB_out_gg(T34, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(0))))
log2D_in_ga(s(s(T12)), T44) → U23_ga(T12, T44, halfB_in_ga(T12, s(s(T26))))
U23_ga(T12, T44, halfB_out_ga(T12, s(s(T26)))) → U24_ga(T12, T44, halfB_in_ga(T26, s(s(T34))))
U24_ga(T12, T44, halfB_out_ga(T26, s(s(T34)))) → U25_ga(T12, T44, halfB_in_ga(T34, s(s(T42))))
U25_ga(T12, T44, halfB_out_ga(T34, s(s(T42)))) → U26_ga(T12, T44, halfB_in_ga(T42, X113))
U26_ga(T12, T44, halfB_out_ga(T42, X113)) → log2D_out_ga(s(s(T12)), T44)
log2D_in_ga(s(s(T12)), s(s(s(s(0))))) → U27_ga(T12, halfB_in_ga(T12, s(s(T26))))
U27_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U28_ga(T12, halfB_in_ga(T26, s(s(T34))))
U28_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U29_ga(T12, halfB_in_ga(T34, s(s(T42))))
U29_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U30_ga(T12, halfB_in_gg(T42, 0))
U30_ga(T12, halfB_out_gg(T42, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(0)))))
U29_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U31_ga(T12, halfB_in_gg(T42, s(0)))
U31_ga(T12, halfB_out_gg(T42, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(0)))))
log2D_in_ga(s(s(T12)), T52) → U32_ga(T12, T52, halfB_in_ga(T12, s(s(T26))))
U32_ga(T12, T52, halfB_out_ga(T12, s(s(T26)))) → U33_ga(T12, T52, halfB_in_ga(T26, s(s(T34))))
U33_ga(T12, T52, halfB_out_ga(T26, s(s(T34)))) → U34_ga(T12, T52, halfB_in_ga(T34, s(s(T42))))
U34_ga(T12, T52, halfB_out_ga(T34, s(s(T42)))) → U35_ga(T12, T52, halfB_in_ga(T42, s(s(T50))))
U35_ga(T12, T52, halfB_out_ga(T42, s(s(T50)))) → U36_ga(T12, T52, halfB_in_ga(T50, X136))
U36_ga(T12, T52, halfB_out_ga(T50, X136)) → log2D_out_ga(s(s(T12)), T52)
log2D_in_ga(s(s(T12)), s(s(s(s(s(0)))))) → U37_ga(T12, halfB_in_ga(T12, s(s(T26))))
U37_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U38_ga(T12, halfB_in_ga(T26, s(s(T34))))
U38_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U39_ga(T12, halfB_in_ga(T34, s(s(T42))))
U39_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U40_ga(T12, halfB_in_ga(T42, s(s(T50))))
U40_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U41_ga(T12, halfB_in_gg(T50, 0))
U41_ga(T12, halfB_out_gg(T50, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(0))))))
U40_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U42_ga(T12, halfB_in_gg(T50, s(0)))
U42_ga(T12, halfB_out_gg(T50, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(0))))))
log2D_in_ga(s(s(T12)), T60) → U43_ga(T12, T60, halfB_in_ga(T12, s(s(T26))))
U43_ga(T12, T60, halfB_out_ga(T12, s(s(T26)))) → U44_ga(T12, T60, halfB_in_ga(T26, s(s(T34))))
U44_ga(T12, T60, halfB_out_ga(T26, s(s(T34)))) → U45_ga(T12, T60, halfB_in_ga(T34, s(s(T42))))
U45_ga(T12, T60, halfB_out_ga(T34, s(s(T42)))) → U46_ga(T12, T60, halfB_in_ga(T42, s(s(T50))))
U46_ga(T12, T60, halfB_out_ga(T42, s(s(T50)))) → U47_ga(T12, T60, halfB_in_ga(T50, s(s(T58))))
U47_ga(T12, T60, halfB_out_ga(T50, s(s(T58)))) → U48_ga(T12, T60, halfB_in_ga(T58, X159))
U48_ga(T12, T60, halfB_out_ga(T58, X159)) → log2D_out_ga(s(s(T12)), T60)
log2D_in_ga(s(s(T12)), s(s(s(s(s(s(0))))))) → U49_ga(T12, halfB_in_ga(T12, s(s(T26))))
U49_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U50_ga(T12, halfB_in_ga(T26, s(s(T34))))
U50_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U51_ga(T12, halfB_in_ga(T34, s(s(T42))))
U51_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U52_ga(T12, halfB_in_ga(T42, s(s(T50))))
U52_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U53_ga(T12, halfB_in_ga(T50, s(s(T58))))
U53_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U54_ga(T12, halfB_in_gg(T58, 0))
U54_ga(T12, halfB_out_gg(T58, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
U53_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U55_ga(T12, halfB_in_gg(T58, s(0)))
U55_ga(T12, halfB_out_gg(T58, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
log2D_in_ga(s(s(T12)), T68) → U56_ga(T12, T68, halfB_in_ga(T12, s(s(T26))))
U56_ga(T12, T68, halfB_out_ga(T12, s(s(T26)))) → U57_ga(T12, T68, halfB_in_ga(T26, s(s(T34))))
U57_ga(T12, T68, halfB_out_ga(T26, s(s(T34)))) → U58_ga(T12, T68, halfB_in_ga(T34, s(s(T42))))
U58_ga(T12, T68, halfB_out_ga(T34, s(s(T42)))) → U59_ga(T12, T68, halfB_in_ga(T42, s(s(T50))))
U59_ga(T12, T68, halfB_out_ga(T42, s(s(T50)))) → U60_ga(T12, T68, halfB_in_ga(T50, s(s(T58))))
U60_ga(T12, T68, halfB_out_ga(T50, s(s(T58)))) → U61_ga(T12, T68, halfB_in_ga(T58, s(s(T66))))
U61_ga(T12, T68, halfB_out_ga(T58, s(s(T66)))) → U62_ga(T12, T68, halfB_in_ga(T66, X182))
U62_ga(T12, T68, halfB_out_ga(T66, X182)) → log2D_out_ga(s(s(T12)), T68)
log2D_in_ga(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → U63_ga(T12, halfB_in_ga(T12, s(s(T26))))
U63_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U64_ga(T12, halfB_in_ga(T26, s(s(T34))))
U64_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U65_ga(T12, halfB_in_ga(T34, s(s(T42))))
U65_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U66_ga(T12, halfB_in_ga(T42, s(s(T50))))
U66_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U67_ga(T12, halfB_in_ga(T50, s(s(T58))))
U67_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U68_ga(T12, halfB_in_ga(T58, s(s(T66))))
U68_ga(T12, halfB_out_ga(T58, s(s(T66)))) → U69_ga(T12, halfB_in_gg(T66, 0))
U69_ga(T12, halfB_out_gg(T66, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
U68_ga(T12, halfB_out_ga(T58, s(s(T66)))) → U70_ga(T12, halfB_in_gg(T66, s(0)))
U70_ga(T12, halfB_out_gg(T66, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
log2D_in_ga(s(s(T12)), T76) → U71_ga(T12, T76, halfB_in_ga(T12, s(s(T26))))
U71_ga(T12, T76, halfB_out_ga(T12, s(s(T26)))) → U72_ga(T12, T76, halfB_in_ga(T26, s(s(T34))))
U72_ga(T12, T76, halfB_out_ga(T26, s(s(T34)))) → U73_ga(T12, T76, halfB_in_ga(T34, s(s(T42))))
U73_ga(T12, T76, halfB_out_ga(T34, s(s(T42)))) → U74_ga(T12, T76, halfB_in_ga(T42, s(s(T50))))
U74_ga(T12, T76, halfB_out_ga(T42, s(s(T50)))) → U75_ga(T12, T76, halfB_in_ga(T50, s(s(T58))))
U75_ga(T12, T76, halfB_out_ga(T50, s(s(T58)))) → U76_ga(T12, T76, halfB_in_ga(T58, s(s(T66))))
U76_ga(T12, T76, halfB_out_ga(T58, s(s(T66)))) → U77_ga(T12, T76, halfB_in_ga(T66, s(s(T74))))
U77_ga(T12, T76, halfB_out_ga(T66, s(s(T74)))) → U78_ga(T12, T76, pC_in_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76))
pC_in_gaga(T74, X205, T77, T76) → U3_gaga(T74, X205, T77, T76, halfB_in_ga(T74, X205))
U3_gaga(T74, X205, T77, T76, halfB_out_ga(T74, X205)) → pC_out_gaga(T74, X205, T77, T76)
pC_in_gaga(T74, 0, T85, s(T85)) → U4_gaga(T74, T85, halfB_in_gg(T74, 0))
U4_gaga(T74, T85, halfB_out_gg(T74, 0)) → pC_out_gaga(T74, 0, T85, s(T85))
pC_in_gaga(T74, s(0), T90, s(T90)) → U5_gaga(T74, T90, halfB_in_gg(T74, s(0)))
U5_gaga(T74, T90, halfB_out_gg(T74, s(0))) → pC_out_gaga(T74, s(0), T90, s(T90))
pC_in_gaga(T74, s(s(T97)), T98, T100) → U6_gaga(T74, T97, T98, T100, halfB_in_ga(T74, s(s(T97))))
U6_gaga(T74, T97, T98, T100, halfB_out_ga(T74, s(s(T97)))) → U7_gaga(T74, T97, T98, T100, pC_in_gaga(T97, X228, s(T98), T100))
U7_gaga(T74, T97, T98, T100, pC_out_gaga(T97, X228, s(T98), T100)) → pC_out_gaga(T74, s(s(T97)), T98, T100)
U78_ga(T12, T76, pC_out_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76)) → log2D_out_ga(s(s(T12)), T76)

The argument filtering Pi contains the following mapping:
log2D_in_ga(x1, x2)  =  log2D_in_ga(x1)
0  =  0
log2D_out_ga(x1, x2)  =  log2D_out_ga
s(x1)  =  s(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
halfB_in_ga(x1, x2)  =  halfB_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
halfA_in_ga(x1, x2)  =  halfA_in_ga(x1)
halfA_out_ga(x1, x2)  =  halfA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
halfB_out_ga(x1, x2)  =  halfB_out_ga(x2)
U9_ga(x1, x2)  =  U9_ga(x2)
halfB_in_gg(x1, x2)  =  halfB_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
halfA_in_gg(x1, x2)  =  halfA_in_gg(x1, x2)
halfA_out_gg(x1, x2)  =  halfA_out_gg
U1_gg(x1, x2, x3)  =  U1_gg(x3)
halfB_out_gg(x1, x2)  =  halfB_out_gg
U10_ga(x1, x2)  =  U10_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2)  =  U13_ga(x2)
U14_ga(x1, x2)  =  U14_ga(x2)
U15_ga(x1, x2)  =  U15_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
U18_ga(x1, x2, x3)  =  U18_ga(x3)
U19_ga(x1, x2)  =  U19_ga(x2)
U20_ga(x1, x2)  =  U20_ga(x2)
U21_ga(x1, x2)  =  U21_ga(x2)
U22_ga(x1, x2)  =  U22_ga(x2)
U23_ga(x1, x2, x3)  =  U23_ga(x3)
U24_ga(x1, x2, x3)  =  U24_ga(x3)
U25_ga(x1, x2, x3)  =  U25_ga(x3)
U26_ga(x1, x2, x3)  =  U26_ga(x3)
U27_ga(x1, x2)  =  U27_ga(x2)
U28_ga(x1, x2)  =  U28_ga(x2)
U29_ga(x1, x2)  =  U29_ga(x2)
U30_ga(x1, x2)  =  U30_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U33_ga(x1, x2, x3)  =  U33_ga(x3)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
U35_ga(x1, x2, x3)  =  U35_ga(x3)
U36_ga(x1, x2, x3)  =  U36_ga(x3)
U37_ga(x1, x2)  =  U37_ga(x2)
U38_ga(x1, x2)  =  U38_ga(x2)
U39_ga(x1, x2)  =  U39_ga(x2)
U40_ga(x1, x2)  =  U40_ga(x2)
U41_ga(x1, x2)  =  U41_ga(x2)
U42_ga(x1, x2)  =  U42_ga(x2)
U43_ga(x1, x2, x3)  =  U43_ga(x3)
U44_ga(x1, x2, x3)  =  U44_ga(x3)
U45_ga(x1, x2, x3)  =  U45_ga(x3)
U46_ga(x1, x2, x3)  =  U46_ga(x3)
U47_ga(x1, x2, x3)  =  U47_ga(x3)
U48_ga(x1, x2, x3)  =  U48_ga(x3)
U49_ga(x1, x2)  =  U49_ga(x2)
U50_ga(x1, x2)  =  U50_ga(x2)
U51_ga(x1, x2)  =  U51_ga(x2)
U52_ga(x1, x2)  =  U52_ga(x2)
U53_ga(x1, x2)  =  U53_ga(x2)
U54_ga(x1, x2)  =  U54_ga(x2)
U55_ga(x1, x2)  =  U55_ga(x2)
U56_ga(x1, x2, x3)  =  U56_ga(x3)
U57_ga(x1, x2, x3)  =  U57_ga(x3)
U58_ga(x1, x2, x3)  =  U58_ga(x3)
U59_ga(x1, x2, x3)  =  U59_ga(x3)
U60_ga(x1, x2, x3)  =  U60_ga(x3)
U61_ga(x1, x2, x3)  =  U61_ga(x3)
U62_ga(x1, x2, x3)  =  U62_ga(x3)
U63_ga(x1, x2)  =  U63_ga(x2)
U64_ga(x1, x2)  =  U64_ga(x2)
U65_ga(x1, x2)  =  U65_ga(x2)
U66_ga(x1, x2)  =  U66_ga(x2)
U67_ga(x1, x2)  =  U67_ga(x2)
U68_ga(x1, x2)  =  U68_ga(x2)
U69_ga(x1, x2)  =  U69_ga(x2)
U70_ga(x1, x2)  =  U70_ga(x2)
U71_ga(x1, x2, x3)  =  U71_ga(x3)
U72_ga(x1, x2, x3)  =  U72_ga(x3)
U73_ga(x1, x2, x3)  =  U73_ga(x3)
U74_ga(x1, x2, x3)  =  U74_ga(x3)
U75_ga(x1, x2, x3)  =  U75_ga(x3)
U76_ga(x1, x2, x3)  =  U76_ga(x3)
U77_ga(x1, x2, x3)  =  U77_ga(x3)
U78_ga(x1, x2, x3)  =  U78_ga(x3)
pC_in_gaga(x1, x2, x3, x4)  =  pC_in_gaga(x1, x3)
U3_gaga(x1, x2, x3, x4, x5)  =  U3_gaga(x5)
pC_out_gaga(x1, x2, x3, x4)  =  pC_out_gaga(x2)
U4_gaga(x1, x2, x3)  =  U4_gaga(x3)
U5_gaga(x1, x2, x3)  =  U5_gaga(x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x3, x5)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x2, x5)
LOG2D_IN_GA(x1, x2)  =  LOG2D_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x3)
HALFB_IN_GA(x1, x2)  =  HALFB_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
HALFA_IN_GA(x1, x2)  =  HALFA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U9_GA(x1, x2)  =  U9_GA(x2)
HALFB_IN_GG(x1, x2)  =  HALFB_IN_GG(x1, x2)
U2_GG(x1, x2, x3)  =  U2_GG(x3)
HALFA_IN_GG(x1, x2)  =  HALFA_IN_GG(x1, x2)
U1_GG(x1, x2, x3)  =  U1_GG(x3)
U10_GA(x1, x2)  =  U10_GA(x2)
U11_GA(x1, x2, x3)  =  U11_GA(x3)
U12_GA(x1, x2, x3)  =  U12_GA(x3)
U13_GA(x1, x2)  =  U13_GA(x2)
U14_GA(x1, x2)  =  U14_GA(x2)
U15_GA(x1, x2)  =  U15_GA(x2)
U16_GA(x1, x2, x3)  =  U16_GA(x3)
U17_GA(x1, x2, x3)  =  U17_GA(x3)
U18_GA(x1, x2, x3)  =  U18_GA(x3)
U19_GA(x1, x2)  =  U19_GA(x2)
U20_GA(x1, x2)  =  U20_GA(x2)
U21_GA(x1, x2)  =  U21_GA(x2)
U22_GA(x1, x2)  =  U22_GA(x2)
U23_GA(x1, x2, x3)  =  U23_GA(x3)
U24_GA(x1, x2, x3)  =  U24_GA(x3)
U25_GA(x1, x2, x3)  =  U25_GA(x3)
U26_GA(x1, x2, x3)  =  U26_GA(x3)
U27_GA(x1, x2)  =  U27_GA(x2)
U28_GA(x1, x2)  =  U28_GA(x2)
U29_GA(x1, x2)  =  U29_GA(x2)
U30_GA(x1, x2)  =  U30_GA(x2)
U31_GA(x1, x2)  =  U31_GA(x2)
U32_GA(x1, x2, x3)  =  U32_GA(x3)
U33_GA(x1, x2, x3)  =  U33_GA(x3)
U34_GA(x1, x2, x3)  =  U34_GA(x3)
U35_GA(x1, x2, x3)  =  U35_GA(x3)
U36_GA(x1, x2, x3)  =  U36_GA(x3)
U37_GA(x1, x2)  =  U37_GA(x2)
U38_GA(x1, x2)  =  U38_GA(x2)
U39_GA(x1, x2)  =  U39_GA(x2)
U40_GA(x1, x2)  =  U40_GA(x2)
U41_GA(x1, x2)  =  U41_GA(x2)
U42_GA(x1, x2)  =  U42_GA(x2)
U43_GA(x1, x2, x3)  =  U43_GA(x3)
U44_GA(x1, x2, x3)  =  U44_GA(x3)
U45_GA(x1, x2, x3)  =  U45_GA(x3)
U46_GA(x1, x2, x3)  =  U46_GA(x3)
U47_GA(x1, x2, x3)  =  U47_GA(x3)
U48_GA(x1, x2, x3)  =  U48_GA(x3)
U49_GA(x1, x2)  =  U49_GA(x2)
U50_GA(x1, x2)  =  U50_GA(x2)
U51_GA(x1, x2)  =  U51_GA(x2)
U52_GA(x1, x2)  =  U52_GA(x2)
U53_GA(x1, x2)  =  U53_GA(x2)
U54_GA(x1, x2)  =  U54_GA(x2)
U55_GA(x1, x2)  =  U55_GA(x2)
U56_GA(x1, x2, x3)  =  U56_GA(x3)
U57_GA(x1, x2, x3)  =  U57_GA(x3)
U58_GA(x1, x2, x3)  =  U58_GA(x3)
U59_GA(x1, x2, x3)  =  U59_GA(x3)
U60_GA(x1, x2, x3)  =  U60_GA(x3)
U61_GA(x1, x2, x3)  =  U61_GA(x3)
U62_GA(x1, x2, x3)  =  U62_GA(x3)
U63_GA(x1, x2)  =  U63_GA(x2)
U64_GA(x1, x2)  =  U64_GA(x2)
U65_GA(x1, x2)  =  U65_GA(x2)
U66_GA(x1, x2)  =  U66_GA(x2)
U67_GA(x1, x2)  =  U67_GA(x2)
U68_GA(x1, x2)  =  U68_GA(x2)
U69_GA(x1, x2)  =  U69_GA(x2)
U70_GA(x1, x2)  =  U70_GA(x2)
U71_GA(x1, x2, x3)  =  U71_GA(x3)
U72_GA(x1, x2, x3)  =  U72_GA(x3)
U73_GA(x1, x2, x3)  =  U73_GA(x3)
U74_GA(x1, x2, x3)  =  U74_GA(x3)
U75_GA(x1, x2, x3)  =  U75_GA(x3)
U76_GA(x1, x2, x3)  =  U76_GA(x3)
U77_GA(x1, x2, x3)  =  U77_GA(x3)
U78_GA(x1, x2, x3)  =  U78_GA(x3)
PC_IN_GAGA(x1, x2, x3, x4)  =  PC_IN_GAGA(x1, x3)
U3_GAGA(x1, x2, x3, x4, x5)  =  U3_GAGA(x5)
U4_GAGA(x1, x2, x3)  =  U4_GAGA(x3)
U5_GAGA(x1, x2, x3)  =  U5_GAGA(x3)
U6_GAGA(x1, x2, x3, x4, x5)  =  U6_GAGA(x3, x5)
U7_GAGA(x1, x2, x3, x4, x5)  =  U7_GAGA(x2, x5)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 150 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

HALFA_IN_GG(s(s(T21)), s(X44)) → HALFA_IN_GG(T21, X44)

The TRS R consists of the following rules:

log2D_in_ga(0, 0) → log2D_out_ga(0, 0)
log2D_in_ga(s(0), 0) → log2D_out_ga(s(0), 0)
log2D_in_ga(s(s(T12)), T14) → U8_ga(T12, T14, halfB_in_ga(T12, X26))
halfB_in_ga(T18, s(X35)) → U2_ga(T18, X35, halfA_in_ga(T18, X35))
halfA_in_ga(0, 0) → halfA_out_ga(0, 0)
halfA_in_ga(s(0), 0) → halfA_out_ga(s(0), 0)
halfA_in_ga(s(s(T21)), s(X44)) → U1_ga(T21, X44, halfA_in_ga(T21, X44))
U1_ga(T21, X44, halfA_out_ga(T21, X44)) → halfA_out_ga(s(s(T21)), s(X44))
U2_ga(T18, X35, halfA_out_ga(T18, X35)) → halfB_out_ga(T18, s(X35))
U8_ga(T12, T14, halfB_out_ga(T12, X26)) → log2D_out_ga(s(s(T12)), T14)
log2D_in_ga(s(s(T12)), s(0)) → U9_ga(T12, halfB_in_gg(T12, 0))
halfB_in_gg(T18, s(X35)) → U2_gg(T18, X35, halfA_in_gg(T18, X35))
halfA_in_gg(0, 0) → halfA_out_gg(0, 0)
halfA_in_gg(s(0), 0) → halfA_out_gg(s(0), 0)
halfA_in_gg(s(s(T21)), s(X44)) → U1_gg(T21, X44, halfA_in_gg(T21, X44))
U1_gg(T21, X44, halfA_out_gg(T21, X44)) → halfA_out_gg(s(s(T21)), s(X44))
U2_gg(T18, X35, halfA_out_gg(T18, X35)) → halfB_out_gg(T18, s(X35))
U9_ga(T12, halfB_out_gg(T12, 0)) → log2D_out_ga(s(s(T12)), s(0))
log2D_in_ga(s(s(T12)), s(0)) → U10_ga(T12, halfB_in_gg(T12, s(0)))
U10_ga(T12, halfB_out_gg(T12, s(0))) → log2D_out_ga(s(s(T12)), s(0))
log2D_in_ga(s(s(T12)), T28) → U11_ga(T12, T28, halfB_in_ga(T12, s(s(T26))))
U11_ga(T12, T28, halfB_out_ga(T12, s(s(T26)))) → U12_ga(T12, T28, halfB_in_ga(T26, X67))
U12_ga(T12, T28, halfB_out_ga(T26, X67)) → log2D_out_ga(s(s(T12)), T28)
log2D_in_ga(s(s(T12)), s(s(0))) → U13_ga(T12, halfB_in_ga(T12, s(s(T26))))
U13_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U14_ga(T12, halfB_in_gg(T26, 0))
U14_ga(T12, halfB_out_gg(T26, 0)) → log2D_out_ga(s(s(T12)), s(s(0)))
U13_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U15_ga(T12, halfB_in_gg(T26, s(0)))
U15_ga(T12, halfB_out_gg(T26, s(0))) → log2D_out_ga(s(s(T12)), s(s(0)))
log2D_in_ga(s(s(T12)), T36) → U16_ga(T12, T36, halfB_in_ga(T12, s(s(T26))))
U16_ga(T12, T36, halfB_out_ga(T12, s(s(T26)))) → U17_ga(T12, T36, halfB_in_ga(T26, s(s(T34))))
U17_ga(T12, T36, halfB_out_ga(T26, s(s(T34)))) → U18_ga(T12, T36, halfB_in_ga(T34, X90))
U18_ga(T12, T36, halfB_out_ga(T34, X90)) → log2D_out_ga(s(s(T12)), T36)
log2D_in_ga(s(s(T12)), s(s(s(0)))) → U19_ga(T12, halfB_in_ga(T12, s(s(T26))))
U19_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U20_ga(T12, halfB_in_ga(T26, s(s(T34))))
U20_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U21_ga(T12, halfB_in_gg(T34, 0))
U21_ga(T12, halfB_out_gg(T34, 0)) → log2D_out_ga(s(s(T12)), s(s(s(0))))
U20_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U22_ga(T12, halfB_in_gg(T34, s(0)))
U22_ga(T12, halfB_out_gg(T34, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(0))))
log2D_in_ga(s(s(T12)), T44) → U23_ga(T12, T44, halfB_in_ga(T12, s(s(T26))))
U23_ga(T12, T44, halfB_out_ga(T12, s(s(T26)))) → U24_ga(T12, T44, halfB_in_ga(T26, s(s(T34))))
U24_ga(T12, T44, halfB_out_ga(T26, s(s(T34)))) → U25_ga(T12, T44, halfB_in_ga(T34, s(s(T42))))
U25_ga(T12, T44, halfB_out_ga(T34, s(s(T42)))) → U26_ga(T12, T44, halfB_in_ga(T42, X113))
U26_ga(T12, T44, halfB_out_ga(T42, X113)) → log2D_out_ga(s(s(T12)), T44)
log2D_in_ga(s(s(T12)), s(s(s(s(0))))) → U27_ga(T12, halfB_in_ga(T12, s(s(T26))))
U27_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U28_ga(T12, halfB_in_ga(T26, s(s(T34))))
U28_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U29_ga(T12, halfB_in_ga(T34, s(s(T42))))
U29_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U30_ga(T12, halfB_in_gg(T42, 0))
U30_ga(T12, halfB_out_gg(T42, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(0)))))
U29_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U31_ga(T12, halfB_in_gg(T42, s(0)))
U31_ga(T12, halfB_out_gg(T42, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(0)))))
log2D_in_ga(s(s(T12)), T52) → U32_ga(T12, T52, halfB_in_ga(T12, s(s(T26))))
U32_ga(T12, T52, halfB_out_ga(T12, s(s(T26)))) → U33_ga(T12, T52, halfB_in_ga(T26, s(s(T34))))
U33_ga(T12, T52, halfB_out_ga(T26, s(s(T34)))) → U34_ga(T12, T52, halfB_in_ga(T34, s(s(T42))))
U34_ga(T12, T52, halfB_out_ga(T34, s(s(T42)))) → U35_ga(T12, T52, halfB_in_ga(T42, s(s(T50))))
U35_ga(T12, T52, halfB_out_ga(T42, s(s(T50)))) → U36_ga(T12, T52, halfB_in_ga(T50, X136))
U36_ga(T12, T52, halfB_out_ga(T50, X136)) → log2D_out_ga(s(s(T12)), T52)
log2D_in_ga(s(s(T12)), s(s(s(s(s(0)))))) → U37_ga(T12, halfB_in_ga(T12, s(s(T26))))
U37_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U38_ga(T12, halfB_in_ga(T26, s(s(T34))))
U38_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U39_ga(T12, halfB_in_ga(T34, s(s(T42))))
U39_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U40_ga(T12, halfB_in_ga(T42, s(s(T50))))
U40_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U41_ga(T12, halfB_in_gg(T50, 0))
U41_ga(T12, halfB_out_gg(T50, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(0))))))
U40_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U42_ga(T12, halfB_in_gg(T50, s(0)))
U42_ga(T12, halfB_out_gg(T50, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(0))))))
log2D_in_ga(s(s(T12)), T60) → U43_ga(T12, T60, halfB_in_ga(T12, s(s(T26))))
U43_ga(T12, T60, halfB_out_ga(T12, s(s(T26)))) → U44_ga(T12, T60, halfB_in_ga(T26, s(s(T34))))
U44_ga(T12, T60, halfB_out_ga(T26, s(s(T34)))) → U45_ga(T12, T60, halfB_in_ga(T34, s(s(T42))))
U45_ga(T12, T60, halfB_out_ga(T34, s(s(T42)))) → U46_ga(T12, T60, halfB_in_ga(T42, s(s(T50))))
U46_ga(T12, T60, halfB_out_ga(T42, s(s(T50)))) → U47_ga(T12, T60, halfB_in_ga(T50, s(s(T58))))
U47_ga(T12, T60, halfB_out_ga(T50, s(s(T58)))) → U48_ga(T12, T60, halfB_in_ga(T58, X159))
U48_ga(T12, T60, halfB_out_ga(T58, X159)) → log2D_out_ga(s(s(T12)), T60)
log2D_in_ga(s(s(T12)), s(s(s(s(s(s(0))))))) → U49_ga(T12, halfB_in_ga(T12, s(s(T26))))
U49_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U50_ga(T12, halfB_in_ga(T26, s(s(T34))))
U50_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U51_ga(T12, halfB_in_ga(T34, s(s(T42))))
U51_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U52_ga(T12, halfB_in_ga(T42, s(s(T50))))
U52_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U53_ga(T12, halfB_in_ga(T50, s(s(T58))))
U53_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U54_ga(T12, halfB_in_gg(T58, 0))
U54_ga(T12, halfB_out_gg(T58, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
U53_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U55_ga(T12, halfB_in_gg(T58, s(0)))
U55_ga(T12, halfB_out_gg(T58, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
log2D_in_ga(s(s(T12)), T68) → U56_ga(T12, T68, halfB_in_ga(T12, s(s(T26))))
U56_ga(T12, T68, halfB_out_ga(T12, s(s(T26)))) → U57_ga(T12, T68, halfB_in_ga(T26, s(s(T34))))
U57_ga(T12, T68, halfB_out_ga(T26, s(s(T34)))) → U58_ga(T12, T68, halfB_in_ga(T34, s(s(T42))))
U58_ga(T12, T68, halfB_out_ga(T34, s(s(T42)))) → U59_ga(T12, T68, halfB_in_ga(T42, s(s(T50))))
U59_ga(T12, T68, halfB_out_ga(T42, s(s(T50)))) → U60_ga(T12, T68, halfB_in_ga(T50, s(s(T58))))
U60_ga(T12, T68, halfB_out_ga(T50, s(s(T58)))) → U61_ga(T12, T68, halfB_in_ga(T58, s(s(T66))))
U61_ga(T12, T68, halfB_out_ga(T58, s(s(T66)))) → U62_ga(T12, T68, halfB_in_ga(T66, X182))
U62_ga(T12, T68, halfB_out_ga(T66, X182)) → log2D_out_ga(s(s(T12)), T68)
log2D_in_ga(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → U63_ga(T12, halfB_in_ga(T12, s(s(T26))))
U63_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U64_ga(T12, halfB_in_ga(T26, s(s(T34))))
U64_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U65_ga(T12, halfB_in_ga(T34, s(s(T42))))
U65_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U66_ga(T12, halfB_in_ga(T42, s(s(T50))))
U66_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U67_ga(T12, halfB_in_ga(T50, s(s(T58))))
U67_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U68_ga(T12, halfB_in_ga(T58, s(s(T66))))
U68_ga(T12, halfB_out_ga(T58, s(s(T66)))) → U69_ga(T12, halfB_in_gg(T66, 0))
U69_ga(T12, halfB_out_gg(T66, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
U68_ga(T12, halfB_out_ga(T58, s(s(T66)))) → U70_ga(T12, halfB_in_gg(T66, s(0)))
U70_ga(T12, halfB_out_gg(T66, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
log2D_in_ga(s(s(T12)), T76) → U71_ga(T12, T76, halfB_in_ga(T12, s(s(T26))))
U71_ga(T12, T76, halfB_out_ga(T12, s(s(T26)))) → U72_ga(T12, T76, halfB_in_ga(T26, s(s(T34))))
U72_ga(T12, T76, halfB_out_ga(T26, s(s(T34)))) → U73_ga(T12, T76, halfB_in_ga(T34, s(s(T42))))
U73_ga(T12, T76, halfB_out_ga(T34, s(s(T42)))) → U74_ga(T12, T76, halfB_in_ga(T42, s(s(T50))))
U74_ga(T12, T76, halfB_out_ga(T42, s(s(T50)))) → U75_ga(T12, T76, halfB_in_ga(T50, s(s(T58))))
U75_ga(T12, T76, halfB_out_ga(T50, s(s(T58)))) → U76_ga(T12, T76, halfB_in_ga(T58, s(s(T66))))
U76_ga(T12, T76, halfB_out_ga(T58, s(s(T66)))) → U77_ga(T12, T76, halfB_in_ga(T66, s(s(T74))))
U77_ga(T12, T76, halfB_out_ga(T66, s(s(T74)))) → U78_ga(T12, T76, pC_in_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76))
pC_in_gaga(T74, X205, T77, T76) → U3_gaga(T74, X205, T77, T76, halfB_in_ga(T74, X205))
U3_gaga(T74, X205, T77, T76, halfB_out_ga(T74, X205)) → pC_out_gaga(T74, X205, T77, T76)
pC_in_gaga(T74, 0, T85, s(T85)) → U4_gaga(T74, T85, halfB_in_gg(T74, 0))
U4_gaga(T74, T85, halfB_out_gg(T74, 0)) → pC_out_gaga(T74, 0, T85, s(T85))
pC_in_gaga(T74, s(0), T90, s(T90)) → U5_gaga(T74, T90, halfB_in_gg(T74, s(0)))
U5_gaga(T74, T90, halfB_out_gg(T74, s(0))) → pC_out_gaga(T74, s(0), T90, s(T90))
pC_in_gaga(T74, s(s(T97)), T98, T100) → U6_gaga(T74, T97, T98, T100, halfB_in_ga(T74, s(s(T97))))
U6_gaga(T74, T97, T98, T100, halfB_out_ga(T74, s(s(T97)))) → U7_gaga(T74, T97, T98, T100, pC_in_gaga(T97, X228, s(T98), T100))
U7_gaga(T74, T97, T98, T100, pC_out_gaga(T97, X228, s(T98), T100)) → pC_out_gaga(T74, s(s(T97)), T98, T100)
U78_ga(T12, T76, pC_out_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76)) → log2D_out_ga(s(s(T12)), T76)

The argument filtering Pi contains the following mapping:
log2D_in_ga(x1, x2)  =  log2D_in_ga(x1)
0  =  0
log2D_out_ga(x1, x2)  =  log2D_out_ga
s(x1)  =  s(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
halfB_in_ga(x1, x2)  =  halfB_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
halfA_in_ga(x1, x2)  =  halfA_in_ga(x1)
halfA_out_ga(x1, x2)  =  halfA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
halfB_out_ga(x1, x2)  =  halfB_out_ga(x2)
U9_ga(x1, x2)  =  U9_ga(x2)
halfB_in_gg(x1, x2)  =  halfB_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
halfA_in_gg(x1, x2)  =  halfA_in_gg(x1, x2)
halfA_out_gg(x1, x2)  =  halfA_out_gg
U1_gg(x1, x2, x3)  =  U1_gg(x3)
halfB_out_gg(x1, x2)  =  halfB_out_gg
U10_ga(x1, x2)  =  U10_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2)  =  U13_ga(x2)
U14_ga(x1, x2)  =  U14_ga(x2)
U15_ga(x1, x2)  =  U15_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
U18_ga(x1, x2, x3)  =  U18_ga(x3)
U19_ga(x1, x2)  =  U19_ga(x2)
U20_ga(x1, x2)  =  U20_ga(x2)
U21_ga(x1, x2)  =  U21_ga(x2)
U22_ga(x1, x2)  =  U22_ga(x2)
U23_ga(x1, x2, x3)  =  U23_ga(x3)
U24_ga(x1, x2, x3)  =  U24_ga(x3)
U25_ga(x1, x2, x3)  =  U25_ga(x3)
U26_ga(x1, x2, x3)  =  U26_ga(x3)
U27_ga(x1, x2)  =  U27_ga(x2)
U28_ga(x1, x2)  =  U28_ga(x2)
U29_ga(x1, x2)  =  U29_ga(x2)
U30_ga(x1, x2)  =  U30_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U33_ga(x1, x2, x3)  =  U33_ga(x3)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
U35_ga(x1, x2, x3)  =  U35_ga(x3)
U36_ga(x1, x2, x3)  =  U36_ga(x3)
U37_ga(x1, x2)  =  U37_ga(x2)
U38_ga(x1, x2)  =  U38_ga(x2)
U39_ga(x1, x2)  =  U39_ga(x2)
U40_ga(x1, x2)  =  U40_ga(x2)
U41_ga(x1, x2)  =  U41_ga(x2)
U42_ga(x1, x2)  =  U42_ga(x2)
U43_ga(x1, x2, x3)  =  U43_ga(x3)
U44_ga(x1, x2, x3)  =  U44_ga(x3)
U45_ga(x1, x2, x3)  =  U45_ga(x3)
U46_ga(x1, x2, x3)  =  U46_ga(x3)
U47_ga(x1, x2, x3)  =  U47_ga(x3)
U48_ga(x1, x2, x3)  =  U48_ga(x3)
U49_ga(x1, x2)  =  U49_ga(x2)
U50_ga(x1, x2)  =  U50_ga(x2)
U51_ga(x1, x2)  =  U51_ga(x2)
U52_ga(x1, x2)  =  U52_ga(x2)
U53_ga(x1, x2)  =  U53_ga(x2)
U54_ga(x1, x2)  =  U54_ga(x2)
U55_ga(x1, x2)  =  U55_ga(x2)
U56_ga(x1, x2, x3)  =  U56_ga(x3)
U57_ga(x1, x2, x3)  =  U57_ga(x3)
U58_ga(x1, x2, x3)  =  U58_ga(x3)
U59_ga(x1, x2, x3)  =  U59_ga(x3)
U60_ga(x1, x2, x3)  =  U60_ga(x3)
U61_ga(x1, x2, x3)  =  U61_ga(x3)
U62_ga(x1, x2, x3)  =  U62_ga(x3)
U63_ga(x1, x2)  =  U63_ga(x2)
U64_ga(x1, x2)  =  U64_ga(x2)
U65_ga(x1, x2)  =  U65_ga(x2)
U66_ga(x1, x2)  =  U66_ga(x2)
U67_ga(x1, x2)  =  U67_ga(x2)
U68_ga(x1, x2)  =  U68_ga(x2)
U69_ga(x1, x2)  =  U69_ga(x2)
U70_ga(x1, x2)  =  U70_ga(x2)
U71_ga(x1, x2, x3)  =  U71_ga(x3)
U72_ga(x1, x2, x3)  =  U72_ga(x3)
U73_ga(x1, x2, x3)  =  U73_ga(x3)
U74_ga(x1, x2, x3)  =  U74_ga(x3)
U75_ga(x1, x2, x3)  =  U75_ga(x3)
U76_ga(x1, x2, x3)  =  U76_ga(x3)
U77_ga(x1, x2, x3)  =  U77_ga(x3)
U78_ga(x1, x2, x3)  =  U78_ga(x3)
pC_in_gaga(x1, x2, x3, x4)  =  pC_in_gaga(x1, x3)
U3_gaga(x1, x2, x3, x4, x5)  =  U3_gaga(x5)
pC_out_gaga(x1, x2, x3, x4)  =  pC_out_gaga(x2)
U4_gaga(x1, x2, x3)  =  U4_gaga(x3)
U5_gaga(x1, x2, x3)  =  U5_gaga(x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x3, x5)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x2, x5)
HALFA_IN_GG(x1, x2)  =  HALFA_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

HALFA_IN_GG(s(s(T21)), s(X44)) → HALFA_IN_GG(T21, X44)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

HALFA_IN_GG(s(s(T21)), s(X44)) → HALFA_IN_GG(T21, X44)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • HALFA_IN_GG(s(s(T21)), s(X44)) → HALFA_IN_GG(T21, X44)
    The graph contains the following edges 1 > 1, 2 > 2

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

HALFA_IN_GA(s(s(T21)), s(X44)) → HALFA_IN_GA(T21, X44)

The TRS R consists of the following rules:

log2D_in_ga(0, 0) → log2D_out_ga(0, 0)
log2D_in_ga(s(0), 0) → log2D_out_ga(s(0), 0)
log2D_in_ga(s(s(T12)), T14) → U8_ga(T12, T14, halfB_in_ga(T12, X26))
halfB_in_ga(T18, s(X35)) → U2_ga(T18, X35, halfA_in_ga(T18, X35))
halfA_in_ga(0, 0) → halfA_out_ga(0, 0)
halfA_in_ga(s(0), 0) → halfA_out_ga(s(0), 0)
halfA_in_ga(s(s(T21)), s(X44)) → U1_ga(T21, X44, halfA_in_ga(T21, X44))
U1_ga(T21, X44, halfA_out_ga(T21, X44)) → halfA_out_ga(s(s(T21)), s(X44))
U2_ga(T18, X35, halfA_out_ga(T18, X35)) → halfB_out_ga(T18, s(X35))
U8_ga(T12, T14, halfB_out_ga(T12, X26)) → log2D_out_ga(s(s(T12)), T14)
log2D_in_ga(s(s(T12)), s(0)) → U9_ga(T12, halfB_in_gg(T12, 0))
halfB_in_gg(T18, s(X35)) → U2_gg(T18, X35, halfA_in_gg(T18, X35))
halfA_in_gg(0, 0) → halfA_out_gg(0, 0)
halfA_in_gg(s(0), 0) → halfA_out_gg(s(0), 0)
halfA_in_gg(s(s(T21)), s(X44)) → U1_gg(T21, X44, halfA_in_gg(T21, X44))
U1_gg(T21, X44, halfA_out_gg(T21, X44)) → halfA_out_gg(s(s(T21)), s(X44))
U2_gg(T18, X35, halfA_out_gg(T18, X35)) → halfB_out_gg(T18, s(X35))
U9_ga(T12, halfB_out_gg(T12, 0)) → log2D_out_ga(s(s(T12)), s(0))
log2D_in_ga(s(s(T12)), s(0)) → U10_ga(T12, halfB_in_gg(T12, s(0)))
U10_ga(T12, halfB_out_gg(T12, s(0))) → log2D_out_ga(s(s(T12)), s(0))
log2D_in_ga(s(s(T12)), T28) → U11_ga(T12, T28, halfB_in_ga(T12, s(s(T26))))
U11_ga(T12, T28, halfB_out_ga(T12, s(s(T26)))) → U12_ga(T12, T28, halfB_in_ga(T26, X67))
U12_ga(T12, T28, halfB_out_ga(T26, X67)) → log2D_out_ga(s(s(T12)), T28)
log2D_in_ga(s(s(T12)), s(s(0))) → U13_ga(T12, halfB_in_ga(T12, s(s(T26))))
U13_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U14_ga(T12, halfB_in_gg(T26, 0))
U14_ga(T12, halfB_out_gg(T26, 0)) → log2D_out_ga(s(s(T12)), s(s(0)))
U13_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U15_ga(T12, halfB_in_gg(T26, s(0)))
U15_ga(T12, halfB_out_gg(T26, s(0))) → log2D_out_ga(s(s(T12)), s(s(0)))
log2D_in_ga(s(s(T12)), T36) → U16_ga(T12, T36, halfB_in_ga(T12, s(s(T26))))
U16_ga(T12, T36, halfB_out_ga(T12, s(s(T26)))) → U17_ga(T12, T36, halfB_in_ga(T26, s(s(T34))))
U17_ga(T12, T36, halfB_out_ga(T26, s(s(T34)))) → U18_ga(T12, T36, halfB_in_ga(T34, X90))
U18_ga(T12, T36, halfB_out_ga(T34, X90)) → log2D_out_ga(s(s(T12)), T36)
log2D_in_ga(s(s(T12)), s(s(s(0)))) → U19_ga(T12, halfB_in_ga(T12, s(s(T26))))
U19_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U20_ga(T12, halfB_in_ga(T26, s(s(T34))))
U20_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U21_ga(T12, halfB_in_gg(T34, 0))
U21_ga(T12, halfB_out_gg(T34, 0)) → log2D_out_ga(s(s(T12)), s(s(s(0))))
U20_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U22_ga(T12, halfB_in_gg(T34, s(0)))
U22_ga(T12, halfB_out_gg(T34, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(0))))
log2D_in_ga(s(s(T12)), T44) → U23_ga(T12, T44, halfB_in_ga(T12, s(s(T26))))
U23_ga(T12, T44, halfB_out_ga(T12, s(s(T26)))) → U24_ga(T12, T44, halfB_in_ga(T26, s(s(T34))))
U24_ga(T12, T44, halfB_out_ga(T26, s(s(T34)))) → U25_ga(T12, T44, halfB_in_ga(T34, s(s(T42))))
U25_ga(T12, T44, halfB_out_ga(T34, s(s(T42)))) → U26_ga(T12, T44, halfB_in_ga(T42, X113))
U26_ga(T12, T44, halfB_out_ga(T42, X113)) → log2D_out_ga(s(s(T12)), T44)
log2D_in_ga(s(s(T12)), s(s(s(s(0))))) → U27_ga(T12, halfB_in_ga(T12, s(s(T26))))
U27_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U28_ga(T12, halfB_in_ga(T26, s(s(T34))))
U28_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U29_ga(T12, halfB_in_ga(T34, s(s(T42))))
U29_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U30_ga(T12, halfB_in_gg(T42, 0))
U30_ga(T12, halfB_out_gg(T42, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(0)))))
U29_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U31_ga(T12, halfB_in_gg(T42, s(0)))
U31_ga(T12, halfB_out_gg(T42, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(0)))))
log2D_in_ga(s(s(T12)), T52) → U32_ga(T12, T52, halfB_in_ga(T12, s(s(T26))))
U32_ga(T12, T52, halfB_out_ga(T12, s(s(T26)))) → U33_ga(T12, T52, halfB_in_ga(T26, s(s(T34))))
U33_ga(T12, T52, halfB_out_ga(T26, s(s(T34)))) → U34_ga(T12, T52, halfB_in_ga(T34, s(s(T42))))
U34_ga(T12, T52, halfB_out_ga(T34, s(s(T42)))) → U35_ga(T12, T52, halfB_in_ga(T42, s(s(T50))))
U35_ga(T12, T52, halfB_out_ga(T42, s(s(T50)))) → U36_ga(T12, T52, halfB_in_ga(T50, X136))
U36_ga(T12, T52, halfB_out_ga(T50, X136)) → log2D_out_ga(s(s(T12)), T52)
log2D_in_ga(s(s(T12)), s(s(s(s(s(0)))))) → U37_ga(T12, halfB_in_ga(T12, s(s(T26))))
U37_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U38_ga(T12, halfB_in_ga(T26, s(s(T34))))
U38_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U39_ga(T12, halfB_in_ga(T34, s(s(T42))))
U39_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U40_ga(T12, halfB_in_ga(T42, s(s(T50))))
U40_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U41_ga(T12, halfB_in_gg(T50, 0))
U41_ga(T12, halfB_out_gg(T50, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(0))))))
U40_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U42_ga(T12, halfB_in_gg(T50, s(0)))
U42_ga(T12, halfB_out_gg(T50, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(0))))))
log2D_in_ga(s(s(T12)), T60) → U43_ga(T12, T60, halfB_in_ga(T12, s(s(T26))))
U43_ga(T12, T60, halfB_out_ga(T12, s(s(T26)))) → U44_ga(T12, T60, halfB_in_ga(T26, s(s(T34))))
U44_ga(T12, T60, halfB_out_ga(T26, s(s(T34)))) → U45_ga(T12, T60, halfB_in_ga(T34, s(s(T42))))
U45_ga(T12, T60, halfB_out_ga(T34, s(s(T42)))) → U46_ga(T12, T60, halfB_in_ga(T42, s(s(T50))))
U46_ga(T12, T60, halfB_out_ga(T42, s(s(T50)))) → U47_ga(T12, T60, halfB_in_ga(T50, s(s(T58))))
U47_ga(T12, T60, halfB_out_ga(T50, s(s(T58)))) → U48_ga(T12, T60, halfB_in_ga(T58, X159))
U48_ga(T12, T60, halfB_out_ga(T58, X159)) → log2D_out_ga(s(s(T12)), T60)
log2D_in_ga(s(s(T12)), s(s(s(s(s(s(0))))))) → U49_ga(T12, halfB_in_ga(T12, s(s(T26))))
U49_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U50_ga(T12, halfB_in_ga(T26, s(s(T34))))
U50_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U51_ga(T12, halfB_in_ga(T34, s(s(T42))))
U51_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U52_ga(T12, halfB_in_ga(T42, s(s(T50))))
U52_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U53_ga(T12, halfB_in_ga(T50, s(s(T58))))
U53_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U54_ga(T12, halfB_in_gg(T58, 0))
U54_ga(T12, halfB_out_gg(T58, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
U53_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U55_ga(T12, halfB_in_gg(T58, s(0)))
U55_ga(T12, halfB_out_gg(T58, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
log2D_in_ga(s(s(T12)), T68) → U56_ga(T12, T68, halfB_in_ga(T12, s(s(T26))))
U56_ga(T12, T68, halfB_out_ga(T12, s(s(T26)))) → U57_ga(T12, T68, halfB_in_ga(T26, s(s(T34))))
U57_ga(T12, T68, halfB_out_ga(T26, s(s(T34)))) → U58_ga(T12, T68, halfB_in_ga(T34, s(s(T42))))
U58_ga(T12, T68, halfB_out_ga(T34, s(s(T42)))) → U59_ga(T12, T68, halfB_in_ga(T42, s(s(T50))))
U59_ga(T12, T68, halfB_out_ga(T42, s(s(T50)))) → U60_ga(T12, T68, halfB_in_ga(T50, s(s(T58))))
U60_ga(T12, T68, halfB_out_ga(T50, s(s(T58)))) → U61_ga(T12, T68, halfB_in_ga(T58, s(s(T66))))
U61_ga(T12, T68, halfB_out_ga(T58, s(s(T66)))) → U62_ga(T12, T68, halfB_in_ga(T66, X182))
U62_ga(T12, T68, halfB_out_ga(T66, X182)) → log2D_out_ga(s(s(T12)), T68)
log2D_in_ga(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → U63_ga(T12, halfB_in_ga(T12, s(s(T26))))
U63_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U64_ga(T12, halfB_in_ga(T26, s(s(T34))))
U64_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U65_ga(T12, halfB_in_ga(T34, s(s(T42))))
U65_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U66_ga(T12, halfB_in_ga(T42, s(s(T50))))
U66_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U67_ga(T12, halfB_in_ga(T50, s(s(T58))))
U67_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U68_ga(T12, halfB_in_ga(T58, s(s(T66))))
U68_ga(T12, halfB_out_ga(T58, s(s(T66)))) → U69_ga(T12, halfB_in_gg(T66, 0))
U69_ga(T12, halfB_out_gg(T66, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
U68_ga(T12, halfB_out_ga(T58, s(s(T66)))) → U70_ga(T12, halfB_in_gg(T66, s(0)))
U70_ga(T12, halfB_out_gg(T66, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
log2D_in_ga(s(s(T12)), T76) → U71_ga(T12, T76, halfB_in_ga(T12, s(s(T26))))
U71_ga(T12, T76, halfB_out_ga(T12, s(s(T26)))) → U72_ga(T12, T76, halfB_in_ga(T26, s(s(T34))))
U72_ga(T12, T76, halfB_out_ga(T26, s(s(T34)))) → U73_ga(T12, T76, halfB_in_ga(T34, s(s(T42))))
U73_ga(T12, T76, halfB_out_ga(T34, s(s(T42)))) → U74_ga(T12, T76, halfB_in_ga(T42, s(s(T50))))
U74_ga(T12, T76, halfB_out_ga(T42, s(s(T50)))) → U75_ga(T12, T76, halfB_in_ga(T50, s(s(T58))))
U75_ga(T12, T76, halfB_out_ga(T50, s(s(T58)))) → U76_ga(T12, T76, halfB_in_ga(T58, s(s(T66))))
U76_ga(T12, T76, halfB_out_ga(T58, s(s(T66)))) → U77_ga(T12, T76, halfB_in_ga(T66, s(s(T74))))
U77_ga(T12, T76, halfB_out_ga(T66, s(s(T74)))) → U78_ga(T12, T76, pC_in_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76))
pC_in_gaga(T74, X205, T77, T76) → U3_gaga(T74, X205, T77, T76, halfB_in_ga(T74, X205))
U3_gaga(T74, X205, T77, T76, halfB_out_ga(T74, X205)) → pC_out_gaga(T74, X205, T77, T76)
pC_in_gaga(T74, 0, T85, s(T85)) → U4_gaga(T74, T85, halfB_in_gg(T74, 0))
U4_gaga(T74, T85, halfB_out_gg(T74, 0)) → pC_out_gaga(T74, 0, T85, s(T85))
pC_in_gaga(T74, s(0), T90, s(T90)) → U5_gaga(T74, T90, halfB_in_gg(T74, s(0)))
U5_gaga(T74, T90, halfB_out_gg(T74, s(0))) → pC_out_gaga(T74, s(0), T90, s(T90))
pC_in_gaga(T74, s(s(T97)), T98, T100) → U6_gaga(T74, T97, T98, T100, halfB_in_ga(T74, s(s(T97))))
U6_gaga(T74, T97, T98, T100, halfB_out_ga(T74, s(s(T97)))) → U7_gaga(T74, T97, T98, T100, pC_in_gaga(T97, X228, s(T98), T100))
U7_gaga(T74, T97, T98, T100, pC_out_gaga(T97, X228, s(T98), T100)) → pC_out_gaga(T74, s(s(T97)), T98, T100)
U78_ga(T12, T76, pC_out_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76)) → log2D_out_ga(s(s(T12)), T76)

The argument filtering Pi contains the following mapping:
log2D_in_ga(x1, x2)  =  log2D_in_ga(x1)
0  =  0
log2D_out_ga(x1, x2)  =  log2D_out_ga
s(x1)  =  s(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
halfB_in_ga(x1, x2)  =  halfB_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
halfA_in_ga(x1, x2)  =  halfA_in_ga(x1)
halfA_out_ga(x1, x2)  =  halfA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
halfB_out_ga(x1, x2)  =  halfB_out_ga(x2)
U9_ga(x1, x2)  =  U9_ga(x2)
halfB_in_gg(x1, x2)  =  halfB_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
halfA_in_gg(x1, x2)  =  halfA_in_gg(x1, x2)
halfA_out_gg(x1, x2)  =  halfA_out_gg
U1_gg(x1, x2, x3)  =  U1_gg(x3)
halfB_out_gg(x1, x2)  =  halfB_out_gg
U10_ga(x1, x2)  =  U10_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2)  =  U13_ga(x2)
U14_ga(x1, x2)  =  U14_ga(x2)
U15_ga(x1, x2)  =  U15_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
U18_ga(x1, x2, x3)  =  U18_ga(x3)
U19_ga(x1, x2)  =  U19_ga(x2)
U20_ga(x1, x2)  =  U20_ga(x2)
U21_ga(x1, x2)  =  U21_ga(x2)
U22_ga(x1, x2)  =  U22_ga(x2)
U23_ga(x1, x2, x3)  =  U23_ga(x3)
U24_ga(x1, x2, x3)  =  U24_ga(x3)
U25_ga(x1, x2, x3)  =  U25_ga(x3)
U26_ga(x1, x2, x3)  =  U26_ga(x3)
U27_ga(x1, x2)  =  U27_ga(x2)
U28_ga(x1, x2)  =  U28_ga(x2)
U29_ga(x1, x2)  =  U29_ga(x2)
U30_ga(x1, x2)  =  U30_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U33_ga(x1, x2, x3)  =  U33_ga(x3)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
U35_ga(x1, x2, x3)  =  U35_ga(x3)
U36_ga(x1, x2, x3)  =  U36_ga(x3)
U37_ga(x1, x2)  =  U37_ga(x2)
U38_ga(x1, x2)  =  U38_ga(x2)
U39_ga(x1, x2)  =  U39_ga(x2)
U40_ga(x1, x2)  =  U40_ga(x2)
U41_ga(x1, x2)  =  U41_ga(x2)
U42_ga(x1, x2)  =  U42_ga(x2)
U43_ga(x1, x2, x3)  =  U43_ga(x3)
U44_ga(x1, x2, x3)  =  U44_ga(x3)
U45_ga(x1, x2, x3)  =  U45_ga(x3)
U46_ga(x1, x2, x3)  =  U46_ga(x3)
U47_ga(x1, x2, x3)  =  U47_ga(x3)
U48_ga(x1, x2, x3)  =  U48_ga(x3)
U49_ga(x1, x2)  =  U49_ga(x2)
U50_ga(x1, x2)  =  U50_ga(x2)
U51_ga(x1, x2)  =  U51_ga(x2)
U52_ga(x1, x2)  =  U52_ga(x2)
U53_ga(x1, x2)  =  U53_ga(x2)
U54_ga(x1, x2)  =  U54_ga(x2)
U55_ga(x1, x2)  =  U55_ga(x2)
U56_ga(x1, x2, x3)  =  U56_ga(x3)
U57_ga(x1, x2, x3)  =  U57_ga(x3)
U58_ga(x1, x2, x3)  =  U58_ga(x3)
U59_ga(x1, x2, x3)  =  U59_ga(x3)
U60_ga(x1, x2, x3)  =  U60_ga(x3)
U61_ga(x1, x2, x3)  =  U61_ga(x3)
U62_ga(x1, x2, x3)  =  U62_ga(x3)
U63_ga(x1, x2)  =  U63_ga(x2)
U64_ga(x1, x2)  =  U64_ga(x2)
U65_ga(x1, x2)  =  U65_ga(x2)
U66_ga(x1, x2)  =  U66_ga(x2)
U67_ga(x1, x2)  =  U67_ga(x2)
U68_ga(x1, x2)  =  U68_ga(x2)
U69_ga(x1, x2)  =  U69_ga(x2)
U70_ga(x1, x2)  =  U70_ga(x2)
U71_ga(x1, x2, x3)  =  U71_ga(x3)
U72_ga(x1, x2, x3)  =  U72_ga(x3)
U73_ga(x1, x2, x3)  =  U73_ga(x3)
U74_ga(x1, x2, x3)  =  U74_ga(x3)
U75_ga(x1, x2, x3)  =  U75_ga(x3)
U76_ga(x1, x2, x3)  =  U76_ga(x3)
U77_ga(x1, x2, x3)  =  U77_ga(x3)
U78_ga(x1, x2, x3)  =  U78_ga(x3)
pC_in_gaga(x1, x2, x3, x4)  =  pC_in_gaga(x1, x3)
U3_gaga(x1, x2, x3, x4, x5)  =  U3_gaga(x5)
pC_out_gaga(x1, x2, x3, x4)  =  pC_out_gaga(x2)
U4_gaga(x1, x2, x3)  =  U4_gaga(x3)
U5_gaga(x1, x2, x3)  =  U5_gaga(x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x3, x5)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x2, x5)
HALFA_IN_GA(x1, x2)  =  HALFA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

HALFA_IN_GA(s(s(T21)), s(X44)) → HALFA_IN_GA(T21, X44)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
HALFA_IN_GA(x1, x2)  =  HALFA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

HALFA_IN_GA(s(s(T21))) → HALFA_IN_GA(T21)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • HALFA_IN_GA(s(s(T21))) → HALFA_IN_GA(T21)
    The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PC_IN_GAGA(T74, s(s(T97)), T98, T100) → U6_GAGA(T74, T97, T98, T100, halfB_in_ga(T74, s(s(T97))))
U6_GAGA(T74, T97, T98, T100, halfB_out_ga(T74, s(s(T97)))) → PC_IN_GAGA(T97, X228, s(T98), T100)

The TRS R consists of the following rules:

log2D_in_ga(0, 0) → log2D_out_ga(0, 0)
log2D_in_ga(s(0), 0) → log2D_out_ga(s(0), 0)
log2D_in_ga(s(s(T12)), T14) → U8_ga(T12, T14, halfB_in_ga(T12, X26))
halfB_in_ga(T18, s(X35)) → U2_ga(T18, X35, halfA_in_ga(T18, X35))
halfA_in_ga(0, 0) → halfA_out_ga(0, 0)
halfA_in_ga(s(0), 0) → halfA_out_ga(s(0), 0)
halfA_in_ga(s(s(T21)), s(X44)) → U1_ga(T21, X44, halfA_in_ga(T21, X44))
U1_ga(T21, X44, halfA_out_ga(T21, X44)) → halfA_out_ga(s(s(T21)), s(X44))
U2_ga(T18, X35, halfA_out_ga(T18, X35)) → halfB_out_ga(T18, s(X35))
U8_ga(T12, T14, halfB_out_ga(T12, X26)) → log2D_out_ga(s(s(T12)), T14)
log2D_in_ga(s(s(T12)), s(0)) → U9_ga(T12, halfB_in_gg(T12, 0))
halfB_in_gg(T18, s(X35)) → U2_gg(T18, X35, halfA_in_gg(T18, X35))
halfA_in_gg(0, 0) → halfA_out_gg(0, 0)
halfA_in_gg(s(0), 0) → halfA_out_gg(s(0), 0)
halfA_in_gg(s(s(T21)), s(X44)) → U1_gg(T21, X44, halfA_in_gg(T21, X44))
U1_gg(T21, X44, halfA_out_gg(T21, X44)) → halfA_out_gg(s(s(T21)), s(X44))
U2_gg(T18, X35, halfA_out_gg(T18, X35)) → halfB_out_gg(T18, s(X35))
U9_ga(T12, halfB_out_gg(T12, 0)) → log2D_out_ga(s(s(T12)), s(0))
log2D_in_ga(s(s(T12)), s(0)) → U10_ga(T12, halfB_in_gg(T12, s(0)))
U10_ga(T12, halfB_out_gg(T12, s(0))) → log2D_out_ga(s(s(T12)), s(0))
log2D_in_ga(s(s(T12)), T28) → U11_ga(T12, T28, halfB_in_ga(T12, s(s(T26))))
U11_ga(T12, T28, halfB_out_ga(T12, s(s(T26)))) → U12_ga(T12, T28, halfB_in_ga(T26, X67))
U12_ga(T12, T28, halfB_out_ga(T26, X67)) → log2D_out_ga(s(s(T12)), T28)
log2D_in_ga(s(s(T12)), s(s(0))) → U13_ga(T12, halfB_in_ga(T12, s(s(T26))))
U13_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U14_ga(T12, halfB_in_gg(T26, 0))
U14_ga(T12, halfB_out_gg(T26, 0)) → log2D_out_ga(s(s(T12)), s(s(0)))
U13_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U15_ga(T12, halfB_in_gg(T26, s(0)))
U15_ga(T12, halfB_out_gg(T26, s(0))) → log2D_out_ga(s(s(T12)), s(s(0)))
log2D_in_ga(s(s(T12)), T36) → U16_ga(T12, T36, halfB_in_ga(T12, s(s(T26))))
U16_ga(T12, T36, halfB_out_ga(T12, s(s(T26)))) → U17_ga(T12, T36, halfB_in_ga(T26, s(s(T34))))
U17_ga(T12, T36, halfB_out_ga(T26, s(s(T34)))) → U18_ga(T12, T36, halfB_in_ga(T34, X90))
U18_ga(T12, T36, halfB_out_ga(T34, X90)) → log2D_out_ga(s(s(T12)), T36)
log2D_in_ga(s(s(T12)), s(s(s(0)))) → U19_ga(T12, halfB_in_ga(T12, s(s(T26))))
U19_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U20_ga(T12, halfB_in_ga(T26, s(s(T34))))
U20_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U21_ga(T12, halfB_in_gg(T34, 0))
U21_ga(T12, halfB_out_gg(T34, 0)) → log2D_out_ga(s(s(T12)), s(s(s(0))))
U20_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U22_ga(T12, halfB_in_gg(T34, s(0)))
U22_ga(T12, halfB_out_gg(T34, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(0))))
log2D_in_ga(s(s(T12)), T44) → U23_ga(T12, T44, halfB_in_ga(T12, s(s(T26))))
U23_ga(T12, T44, halfB_out_ga(T12, s(s(T26)))) → U24_ga(T12, T44, halfB_in_ga(T26, s(s(T34))))
U24_ga(T12, T44, halfB_out_ga(T26, s(s(T34)))) → U25_ga(T12, T44, halfB_in_ga(T34, s(s(T42))))
U25_ga(T12, T44, halfB_out_ga(T34, s(s(T42)))) → U26_ga(T12, T44, halfB_in_ga(T42, X113))
U26_ga(T12, T44, halfB_out_ga(T42, X113)) → log2D_out_ga(s(s(T12)), T44)
log2D_in_ga(s(s(T12)), s(s(s(s(0))))) → U27_ga(T12, halfB_in_ga(T12, s(s(T26))))
U27_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U28_ga(T12, halfB_in_ga(T26, s(s(T34))))
U28_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U29_ga(T12, halfB_in_ga(T34, s(s(T42))))
U29_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U30_ga(T12, halfB_in_gg(T42, 0))
U30_ga(T12, halfB_out_gg(T42, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(0)))))
U29_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U31_ga(T12, halfB_in_gg(T42, s(0)))
U31_ga(T12, halfB_out_gg(T42, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(0)))))
log2D_in_ga(s(s(T12)), T52) → U32_ga(T12, T52, halfB_in_ga(T12, s(s(T26))))
U32_ga(T12, T52, halfB_out_ga(T12, s(s(T26)))) → U33_ga(T12, T52, halfB_in_ga(T26, s(s(T34))))
U33_ga(T12, T52, halfB_out_ga(T26, s(s(T34)))) → U34_ga(T12, T52, halfB_in_ga(T34, s(s(T42))))
U34_ga(T12, T52, halfB_out_ga(T34, s(s(T42)))) → U35_ga(T12, T52, halfB_in_ga(T42, s(s(T50))))
U35_ga(T12, T52, halfB_out_ga(T42, s(s(T50)))) → U36_ga(T12, T52, halfB_in_ga(T50, X136))
U36_ga(T12, T52, halfB_out_ga(T50, X136)) → log2D_out_ga(s(s(T12)), T52)
log2D_in_ga(s(s(T12)), s(s(s(s(s(0)))))) → U37_ga(T12, halfB_in_ga(T12, s(s(T26))))
U37_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U38_ga(T12, halfB_in_ga(T26, s(s(T34))))
U38_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U39_ga(T12, halfB_in_ga(T34, s(s(T42))))
U39_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U40_ga(T12, halfB_in_ga(T42, s(s(T50))))
U40_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U41_ga(T12, halfB_in_gg(T50, 0))
U41_ga(T12, halfB_out_gg(T50, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(0))))))
U40_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U42_ga(T12, halfB_in_gg(T50, s(0)))
U42_ga(T12, halfB_out_gg(T50, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(0))))))
log2D_in_ga(s(s(T12)), T60) → U43_ga(T12, T60, halfB_in_ga(T12, s(s(T26))))
U43_ga(T12, T60, halfB_out_ga(T12, s(s(T26)))) → U44_ga(T12, T60, halfB_in_ga(T26, s(s(T34))))
U44_ga(T12, T60, halfB_out_ga(T26, s(s(T34)))) → U45_ga(T12, T60, halfB_in_ga(T34, s(s(T42))))
U45_ga(T12, T60, halfB_out_ga(T34, s(s(T42)))) → U46_ga(T12, T60, halfB_in_ga(T42, s(s(T50))))
U46_ga(T12, T60, halfB_out_ga(T42, s(s(T50)))) → U47_ga(T12, T60, halfB_in_ga(T50, s(s(T58))))
U47_ga(T12, T60, halfB_out_ga(T50, s(s(T58)))) → U48_ga(T12, T60, halfB_in_ga(T58, X159))
U48_ga(T12, T60, halfB_out_ga(T58, X159)) → log2D_out_ga(s(s(T12)), T60)
log2D_in_ga(s(s(T12)), s(s(s(s(s(s(0))))))) → U49_ga(T12, halfB_in_ga(T12, s(s(T26))))
U49_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U50_ga(T12, halfB_in_ga(T26, s(s(T34))))
U50_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U51_ga(T12, halfB_in_ga(T34, s(s(T42))))
U51_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U52_ga(T12, halfB_in_ga(T42, s(s(T50))))
U52_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U53_ga(T12, halfB_in_ga(T50, s(s(T58))))
U53_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U54_ga(T12, halfB_in_gg(T58, 0))
U54_ga(T12, halfB_out_gg(T58, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
U53_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U55_ga(T12, halfB_in_gg(T58, s(0)))
U55_ga(T12, halfB_out_gg(T58, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
log2D_in_ga(s(s(T12)), T68) → U56_ga(T12, T68, halfB_in_ga(T12, s(s(T26))))
U56_ga(T12, T68, halfB_out_ga(T12, s(s(T26)))) → U57_ga(T12, T68, halfB_in_ga(T26, s(s(T34))))
U57_ga(T12, T68, halfB_out_ga(T26, s(s(T34)))) → U58_ga(T12, T68, halfB_in_ga(T34, s(s(T42))))
U58_ga(T12, T68, halfB_out_ga(T34, s(s(T42)))) → U59_ga(T12, T68, halfB_in_ga(T42, s(s(T50))))
U59_ga(T12, T68, halfB_out_ga(T42, s(s(T50)))) → U60_ga(T12, T68, halfB_in_ga(T50, s(s(T58))))
U60_ga(T12, T68, halfB_out_ga(T50, s(s(T58)))) → U61_ga(T12, T68, halfB_in_ga(T58, s(s(T66))))
U61_ga(T12, T68, halfB_out_ga(T58, s(s(T66)))) → U62_ga(T12, T68, halfB_in_ga(T66, X182))
U62_ga(T12, T68, halfB_out_ga(T66, X182)) → log2D_out_ga(s(s(T12)), T68)
log2D_in_ga(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → U63_ga(T12, halfB_in_ga(T12, s(s(T26))))
U63_ga(T12, halfB_out_ga(T12, s(s(T26)))) → U64_ga(T12, halfB_in_ga(T26, s(s(T34))))
U64_ga(T12, halfB_out_ga(T26, s(s(T34)))) → U65_ga(T12, halfB_in_ga(T34, s(s(T42))))
U65_ga(T12, halfB_out_ga(T34, s(s(T42)))) → U66_ga(T12, halfB_in_ga(T42, s(s(T50))))
U66_ga(T12, halfB_out_ga(T42, s(s(T50)))) → U67_ga(T12, halfB_in_ga(T50, s(s(T58))))
U67_ga(T12, halfB_out_ga(T50, s(s(T58)))) → U68_ga(T12, halfB_in_ga(T58, s(s(T66))))
U68_ga(T12, halfB_out_ga(T58, s(s(T66)))) → U69_ga(T12, halfB_in_gg(T66, 0))
U69_ga(T12, halfB_out_gg(T66, 0)) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
U68_ga(T12, halfB_out_ga(T58, s(s(T66)))) → U70_ga(T12, halfB_in_gg(T66, s(0)))
U70_ga(T12, halfB_out_gg(T66, s(0))) → log2D_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
log2D_in_ga(s(s(T12)), T76) → U71_ga(T12, T76, halfB_in_ga(T12, s(s(T26))))
U71_ga(T12, T76, halfB_out_ga(T12, s(s(T26)))) → U72_ga(T12, T76, halfB_in_ga(T26, s(s(T34))))
U72_ga(T12, T76, halfB_out_ga(T26, s(s(T34)))) → U73_ga(T12, T76, halfB_in_ga(T34, s(s(T42))))
U73_ga(T12, T76, halfB_out_ga(T34, s(s(T42)))) → U74_ga(T12, T76, halfB_in_ga(T42, s(s(T50))))
U74_ga(T12, T76, halfB_out_ga(T42, s(s(T50)))) → U75_ga(T12, T76, halfB_in_ga(T50, s(s(T58))))
U75_ga(T12, T76, halfB_out_ga(T50, s(s(T58)))) → U76_ga(T12, T76, halfB_in_ga(T58, s(s(T66))))
U76_ga(T12, T76, halfB_out_ga(T58, s(s(T66)))) → U77_ga(T12, T76, halfB_in_ga(T66, s(s(T74))))
U77_ga(T12, T76, halfB_out_ga(T66, s(s(T74)))) → U78_ga(T12, T76, pC_in_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76))
pC_in_gaga(T74, X205, T77, T76) → U3_gaga(T74, X205, T77, T76, halfB_in_ga(T74, X205))
U3_gaga(T74, X205, T77, T76, halfB_out_ga(T74, X205)) → pC_out_gaga(T74, X205, T77, T76)
pC_in_gaga(T74, 0, T85, s(T85)) → U4_gaga(T74, T85, halfB_in_gg(T74, 0))
U4_gaga(T74, T85, halfB_out_gg(T74, 0)) → pC_out_gaga(T74, 0, T85, s(T85))
pC_in_gaga(T74, s(0), T90, s(T90)) → U5_gaga(T74, T90, halfB_in_gg(T74, s(0)))
U5_gaga(T74, T90, halfB_out_gg(T74, s(0))) → pC_out_gaga(T74, s(0), T90, s(T90))
pC_in_gaga(T74, s(s(T97)), T98, T100) → U6_gaga(T74, T97, T98, T100, halfB_in_ga(T74, s(s(T97))))
U6_gaga(T74, T97, T98, T100, halfB_out_ga(T74, s(s(T97)))) → U7_gaga(T74, T97, T98, T100, pC_in_gaga(T97, X228, s(T98), T100))
U7_gaga(T74, T97, T98, T100, pC_out_gaga(T97, X228, s(T98), T100)) → pC_out_gaga(T74, s(s(T97)), T98, T100)
U78_ga(T12, T76, pC_out_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76)) → log2D_out_ga(s(s(T12)), T76)

The argument filtering Pi contains the following mapping:
log2D_in_ga(x1, x2)  =  log2D_in_ga(x1)
0  =  0
log2D_out_ga(x1, x2)  =  log2D_out_ga
s(x1)  =  s(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
halfB_in_ga(x1, x2)  =  halfB_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
halfA_in_ga(x1, x2)  =  halfA_in_ga(x1)
halfA_out_ga(x1, x2)  =  halfA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
halfB_out_ga(x1, x2)  =  halfB_out_ga(x2)
U9_ga(x1, x2)  =  U9_ga(x2)
halfB_in_gg(x1, x2)  =  halfB_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
halfA_in_gg(x1, x2)  =  halfA_in_gg(x1, x2)
halfA_out_gg(x1, x2)  =  halfA_out_gg
U1_gg(x1, x2, x3)  =  U1_gg(x3)
halfB_out_gg(x1, x2)  =  halfB_out_gg
U10_ga(x1, x2)  =  U10_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2)  =  U13_ga(x2)
U14_ga(x1, x2)  =  U14_ga(x2)
U15_ga(x1, x2)  =  U15_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
U18_ga(x1, x2, x3)  =  U18_ga(x3)
U19_ga(x1, x2)  =  U19_ga(x2)
U20_ga(x1, x2)  =  U20_ga(x2)
U21_ga(x1, x2)  =  U21_ga(x2)
U22_ga(x1, x2)  =  U22_ga(x2)
U23_ga(x1, x2, x3)  =  U23_ga(x3)
U24_ga(x1, x2, x3)  =  U24_ga(x3)
U25_ga(x1, x2, x3)  =  U25_ga(x3)
U26_ga(x1, x2, x3)  =  U26_ga(x3)
U27_ga(x1, x2)  =  U27_ga(x2)
U28_ga(x1, x2)  =  U28_ga(x2)
U29_ga(x1, x2)  =  U29_ga(x2)
U30_ga(x1, x2)  =  U30_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U33_ga(x1, x2, x3)  =  U33_ga(x3)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
U35_ga(x1, x2, x3)  =  U35_ga(x3)
U36_ga(x1, x2, x3)  =  U36_ga(x3)
U37_ga(x1, x2)  =  U37_ga(x2)
U38_ga(x1, x2)  =  U38_ga(x2)
U39_ga(x1, x2)  =  U39_ga(x2)
U40_ga(x1, x2)  =  U40_ga(x2)
U41_ga(x1, x2)  =  U41_ga(x2)
U42_ga(x1, x2)  =  U42_ga(x2)
U43_ga(x1, x2, x3)  =  U43_ga(x3)
U44_ga(x1, x2, x3)  =  U44_ga(x3)
U45_ga(x1, x2, x3)  =  U45_ga(x3)
U46_ga(x1, x2, x3)  =  U46_ga(x3)
U47_ga(x1, x2, x3)  =  U47_ga(x3)
U48_ga(x1, x2, x3)  =  U48_ga(x3)
U49_ga(x1, x2)  =  U49_ga(x2)
U50_ga(x1, x2)  =  U50_ga(x2)
U51_ga(x1, x2)  =  U51_ga(x2)
U52_ga(x1, x2)  =  U52_ga(x2)
U53_ga(x1, x2)  =  U53_ga(x2)
U54_ga(x1, x2)  =  U54_ga(x2)
U55_ga(x1, x2)  =  U55_ga(x2)
U56_ga(x1, x2, x3)  =  U56_ga(x3)
U57_ga(x1, x2, x3)  =  U57_ga(x3)
U58_ga(x1, x2, x3)  =  U58_ga(x3)
U59_ga(x1, x2, x3)  =  U59_ga(x3)
U60_ga(x1, x2, x3)  =  U60_ga(x3)
U61_ga(x1, x2, x3)  =  U61_ga(x3)
U62_ga(x1, x2, x3)  =  U62_ga(x3)
U63_ga(x1, x2)  =  U63_ga(x2)
U64_ga(x1, x2)  =  U64_ga(x2)
U65_ga(x1, x2)  =  U65_ga(x2)
U66_ga(x1, x2)  =  U66_ga(x2)
U67_ga(x1, x2)  =  U67_ga(x2)
U68_ga(x1, x2)  =  U68_ga(x2)
U69_ga(x1, x2)  =  U69_ga(x2)
U70_ga(x1, x2)  =  U70_ga(x2)
U71_ga(x1, x2, x3)  =  U71_ga(x3)
U72_ga(x1, x2, x3)  =  U72_ga(x3)
U73_ga(x1, x2, x3)  =  U73_ga(x3)
U74_ga(x1, x2, x3)  =  U74_ga(x3)
U75_ga(x1, x2, x3)  =  U75_ga(x3)
U76_ga(x1, x2, x3)  =  U76_ga(x3)
U77_ga(x1, x2, x3)  =  U77_ga(x3)
U78_ga(x1, x2, x3)  =  U78_ga(x3)
pC_in_gaga(x1, x2, x3, x4)  =  pC_in_gaga(x1, x3)
U3_gaga(x1, x2, x3, x4, x5)  =  U3_gaga(x5)
pC_out_gaga(x1, x2, x3, x4)  =  pC_out_gaga(x2)
U4_gaga(x1, x2, x3)  =  U4_gaga(x3)
U5_gaga(x1, x2, x3)  =  U5_gaga(x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x3, x5)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x2, x5)
PC_IN_GAGA(x1, x2, x3, x4)  =  PC_IN_GAGA(x1, x3)
U6_GAGA(x1, x2, x3, x4, x5)  =  U6_GAGA(x3, x5)

We have to consider all (P,R,Pi)-chains

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PC_IN_GAGA(T74, s(s(T97)), T98, T100) → U6_GAGA(T74, T97, T98, T100, halfB_in_ga(T74, s(s(T97))))
U6_GAGA(T74, T97, T98, T100, halfB_out_ga(T74, s(s(T97)))) → PC_IN_GAGA(T97, X228, s(T98), T100)

The TRS R consists of the following rules:

halfB_in_ga(T18, s(X35)) → U2_ga(T18, X35, halfA_in_ga(T18, X35))
U2_ga(T18, X35, halfA_out_ga(T18, X35)) → halfB_out_ga(T18, s(X35))
halfA_in_ga(0, 0) → halfA_out_ga(0, 0)
halfA_in_ga(s(0), 0) → halfA_out_ga(s(0), 0)
halfA_in_ga(s(s(T21)), s(X44)) → U1_ga(T21, X44, halfA_in_ga(T21, X44))
U1_ga(T21, X44, halfA_out_ga(T21, X44)) → halfA_out_ga(s(s(T21)), s(X44))

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
halfB_in_ga(x1, x2)  =  halfB_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
halfA_in_ga(x1, x2)  =  halfA_in_ga(x1)
halfA_out_ga(x1, x2)  =  halfA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
halfB_out_ga(x1, x2)  =  halfB_out_ga(x2)
PC_IN_GAGA(x1, x2, x3, x4)  =  PC_IN_GAGA(x1, x3)
U6_GAGA(x1, x2, x3, x4, x5)  =  U6_GAGA(x3, x5)

We have to consider all (P,R,Pi)-chains

(26) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PC_IN_GAGA(T74, T98) → U6_GAGA(T98, halfB_in_ga(T74))
U6_GAGA(T98, halfB_out_ga(s(s(T97)))) → PC_IN_GAGA(T97, s(T98))

The TRS R consists of the following rules:

halfB_in_ga(T18) → U2_ga(halfA_in_ga(T18))
U2_ga(halfA_out_ga(X35)) → halfB_out_ga(s(X35))
halfA_in_ga(0) → halfA_out_ga(0)
halfA_in_ga(s(0)) → halfA_out_ga(0)
halfA_in_ga(s(s(T21))) → U1_ga(halfA_in_ga(T21))
U1_ga(halfA_out_ga(X44)) → halfA_out_ga(s(X44))

The set Q consists of the following terms:

halfB_in_ga(x0)
U2_ga(x0)
halfA_in_ga(x0)
U1_ga(x0)

We have to consider all (P,Q,R)-chains.

(28) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

U6_GAGA(T98, halfB_out_ga(s(s(T97)))) → PC_IN_GAGA(T97, s(T98))

Strictly oriented rules of the TRS R:

halfA_in_ga(s(0)) → halfA_out_ga(0)

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(PC_IN_GAGA(x1, x2)) = 2 + 2·x1 + x2   
POL(U1_ga(x1)) = 2 + x1   
POL(U2_ga(x1)) = 1 + x1   
POL(U6_GAGA(x1, x2)) = x1 + 2·x2   
POL(halfA_in_ga(x1)) = x1   
POL(halfA_out_ga(x1)) = 2·x1   
POL(halfB_in_ga(x1)) = 1 + x1   
POL(halfB_out_ga(x1)) = x1   
POL(s(x1)) = 1 + x1   

(29) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PC_IN_GAGA(T74, T98) → U6_GAGA(T98, halfB_in_ga(T74))

The TRS R consists of the following rules:

halfB_in_ga(T18) → U2_ga(halfA_in_ga(T18))
U2_ga(halfA_out_ga(X35)) → halfB_out_ga(s(X35))
halfA_in_ga(0) → halfA_out_ga(0)
halfA_in_ga(s(s(T21))) → U1_ga(halfA_in_ga(T21))
U1_ga(halfA_out_ga(X44)) → halfA_out_ga(s(X44))

The set Q consists of the following terms:

halfB_in_ga(x0)
U2_ga(x0)
halfA_in_ga(x0)
U1_ga(x0)

We have to consider all (P,Q,R)-chains.

(30) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(31) TRUE